Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  bj-inf2vnlem2 Structured version   GIF version

Theorem bj-inf2vnlem2 7385
Description: Lemma for bj-inf2vnlem3 7386 and bj-inf2vnlem4 7387. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
Assertion
Ref Expression
bj-inf2vnlem2 (x A (x = ∅ y A x = suc y) → (Ind 𝑍u(𝑡 u (𝑡 A𝑡 𝑍) → (u Au 𝑍))))
Distinct variable groups:   x,y,𝑡,u,A   x,𝑍,y,𝑡,u

Proof of Theorem bj-inf2vnlem2
Dummy variable v is distinct from all other variables.
StepHypRef Expression
1 eqeq1 2024 . . . . . . 7 (x = u → (x = ∅ ↔ u = ∅))
2 eqeq1 2024 . . . . . . . 8 (x = u → (x = suc yu = suc y))
32rexbidv 2301 . . . . . . 7 (x = u → (y A x = suc yy A u = suc y))
41, 3orbi12d 694 . . . . . 6 (x = u → ((x = ∅ y A x = suc y) ↔ (u = ∅ y A u = suc y)))
54rspcv 2625 . . . . 5 (u A → (x A (x = ∅ y A x = suc y) → (u = ∅ y A u = suc y)))
6 df-bj-ind 7346 . . . . . . . . 9 (Ind 𝑍 ↔ (∅ 𝑍 v 𝑍 suc v 𝑍))
76simplbi 259 . . . . . . . 8 (Ind 𝑍 → ∅ 𝑍)
8 eleq1 2078 . . . . . . . 8 (u = ∅ → (u 𝑍 ↔ ∅ 𝑍))
97, 8syl5ibr 145 . . . . . . 7 (u = ∅ → (Ind 𝑍u 𝑍))
109a1dd 42 . . . . . 6 (u = ∅ → (Ind 𝑍 → (𝑡 u (𝑡 A𝑡 𝑍) → u 𝑍)))
11 vex 2534 . . . . . . . . . 10 y V
1211sucid 4099 . . . . . . . . 9 y suc y
13 eleq2 2079 . . . . . . . . . 10 (suc y = u → (y suc yy u))
1413eqcoms 2021 . . . . . . . . 9 (u = suc y → (y suc yy u))
1512, 14mpbii 136 . . . . . . . 8 (u = suc yy u)
16 eleq1 2078 . . . . . . . . . . . . 13 (𝑡 = y → (𝑡 Ay A))
17 eleq1 2078 . . . . . . . . . . . . 13 (𝑡 = y → (𝑡 𝑍y 𝑍))
1816, 17imbi12d 223 . . . . . . . . . . . 12 (𝑡 = y → ((𝑡 A𝑡 𝑍) ↔ (y Ay 𝑍)))
1918rspcv 2625 . . . . . . . . . . 11 (y u → (𝑡 u (𝑡 A𝑡 𝑍) → (y Ay 𝑍)))
20 bj-indsuc 7347 . . . . . . . . . . . 12 (Ind 𝑍 → (y 𝑍 → suc y 𝑍))
21 eleq1a 2087 . . . . . . . . . . . 12 (suc y 𝑍 → (u = suc yu 𝑍))
2220, 21syl6com 31 . . . . . . . . . . 11 (y 𝑍 → (Ind 𝑍 → (u = suc yu 𝑍)))
2319, 22syl8 65 . . . . . . . . . 10 (y u → (𝑡 u (𝑡 A𝑡 𝑍) → (y A → (Ind 𝑍 → (u = suc yu 𝑍)))))
2423com13 74 . . . . . . . . 9 (y A → (𝑡 u (𝑡 A𝑡 𝑍) → (y u → (Ind 𝑍 → (u = suc yu 𝑍)))))
2524com25 85 . . . . . . . 8 (y A → (u = suc y → (y u → (Ind 𝑍 → (𝑡 u (𝑡 A𝑡 𝑍) → u 𝑍)))))
2615, 25mpdi 38 . . . . . . 7 (y A → (u = suc y → (Ind 𝑍 → (𝑡 u (𝑡 A𝑡 𝑍) → u 𝑍))))
2726rexlimiv 2401 . . . . . 6 (y A u = suc y → (Ind 𝑍 → (𝑡 u (𝑡 A𝑡 𝑍) → u 𝑍)))
2810, 27jaoi 623 . . . . 5 ((u = ∅ y A u = suc y) → (Ind 𝑍 → (𝑡 u (𝑡 A𝑡 𝑍) → u 𝑍)))
295, 28syl6 29 . . . 4 (u A → (x A (x = ∅ y A x = suc y) → (Ind 𝑍 → (𝑡 u (𝑡 A𝑡 𝑍) → u 𝑍))))
3029com3l 75 . . 3 (x A (x = ∅ y A x = suc y) → (Ind 𝑍 → (u A → (𝑡 u (𝑡 A𝑡 𝑍) → u 𝑍))))
3130alrimdv 1734 . 2 (x A (x = ∅ y A x = suc y) → (Ind 𝑍u(u A → (𝑡 u (𝑡 A𝑡 𝑍) → u 𝑍))))
32 bi2.04 237 . . 3 ((u A → (𝑡 u (𝑡 A𝑡 𝑍) → u 𝑍)) ↔ (𝑡 u (𝑡 A𝑡 𝑍) → (u Au 𝑍)))
3332albii 1335 . 2 (u(u A → (𝑡 u (𝑡 A𝑡 𝑍) → u 𝑍)) ↔ u(𝑡 u (𝑡 A𝑡 𝑍) → (u Au 𝑍)))
3431, 33syl6ib 150 1 (x A (x = ∅ y A x = suc y) → (Ind 𝑍u(𝑡 u (𝑡 A𝑡 𝑍) → (u Au 𝑍))))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   wo 616  wal 1224   = wceq 1226   wcel 1370  wral 2280  wrex 2281  c0 3197  suc csuc 4047  Ind wind 7345
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000
This theorem depends on definitions:  df-bi 110  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-v 2533  df-un 2895  df-sn 3352  df-suc 4053  df-bj-ind 7346
This theorem is referenced by:  bj-inf2vnlem3  7386  bj-inf2vnlem4  7387
  Copyright terms: Public domain W3C validator