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 9401
Description: Lemma for bj-inf2vnlem3 9402 and bj-inf2vnlem4 9403. 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 2043 . . . . . . 7 (x = u → (x = ∅ ↔ u = ∅))
2 eqeq1 2043 . . . . . . . 8 (x = u → (x = suc yu = suc y))
32rexbidv 2321 . . . . . . 7 (x = u → (y A x = suc yy A u = suc y))
41, 3orbi12d 706 . . . . . 6 (x = u → ((x = ∅ y A x = suc y) ↔ (u = ∅ y A u = suc y)))
54rspcv 2646 . . . . 5 (u A → (x A (x = ∅ y A x = suc y) → (u = ∅ y A u = suc y)))
6 df-bj-ind 9362 . . . . . . . . 9 (Ind 𝑍 ↔ (∅ 𝑍 v 𝑍 suc v 𝑍))
76simplbi 259 . . . . . . . 8 (Ind 𝑍 → ∅ 𝑍)
8 eleq1 2097 . . . . . . . 8 (u = ∅ → (u 𝑍 ↔ ∅ 𝑍))
97, 8syl5ibr 145 . . . . . . 7 (u = ∅ → (Ind 𝑍u 𝑍))
109a1dd 42 . . . . . 6 (u = ∅ → (Ind 𝑍 → (𝑡 u (𝑡 A𝑡 𝑍) → u 𝑍)))
11 vex 2554 . . . . . . . . . 10 y V
1211sucid 4120 . . . . . . . . 9 y suc y
13 eleq2 2098 . . . . . . . . . 10 (suc y = u → (y suc yy u))
1413eqcoms 2040 . . . . . . . . 9 (u = suc y → (y suc yy u))
1512, 14mpbii 136 . . . . . . . 8 (u = suc yy u)
16 eleq1 2097 . . . . . . . . . . . . 13 (𝑡 = y → (𝑡 Ay A))
17 eleq1 2097 . . . . . . . . . . . . 13 (𝑡 = y → (𝑡 𝑍y 𝑍))
1816, 17imbi12d 223 . . . . . . . . . . . 12 (𝑡 = y → ((𝑡 A𝑡 𝑍) ↔ (y Ay 𝑍)))
1918rspcv 2646 . . . . . . . . . . 11 (y u → (𝑡 u (𝑡 A𝑡 𝑍) → (y Ay 𝑍)))
20 bj-indsuc 9363 . . . . . . . . . . . 12 (Ind 𝑍 → (y 𝑍 → suc y 𝑍))
21 eleq1a 2106 . . . . . . . . . . . 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 2421 . . . . . 6 (y A u = suc y → (Ind 𝑍 → (𝑡 u (𝑡 A𝑡 𝑍) → u 𝑍)))
2810, 27jaoi 635 . . . . 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 1753 . 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 1356 . 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 628  wal 1240   = wceq 1242   wcel 1390  wral 2300  wrex 2301  c0 3218  suc csuc 4068  Ind wind 9361
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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-sn 3373  df-suc 4074  df-bj-ind 9362
This theorem is referenced by:  bj-inf2vnlem3  9402  bj-inf2vnlem4  9403
  Copyright terms: Public domain W3C validator