Theorem bj-inf2vnlem2 9431

Description: Lemma for bj-inf2vnlem3 9432 and bj-inf2vnlem4 9433. 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 ∈ A → u ∈ 𝑍))))

Distinct variable groups:   x,y,𝑡,u,A   x,𝑍,y,𝑡,u

Proof of Theorem bj-inf2vnlem2

Dummy variable v is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1 2043	. . . . . . 7 ⊢ (x = u → (x = ∅ ↔ u = ∅))
2		eqeq1 2043	. . . . . . . 8 ⊢ (x = u → (x = suc y ↔ u = suc y))
3	2	rexbidv 2321	. . . . . . 7 ⊢ (x = u → (∃y ∈ A x = suc y ↔ ∃y ∈ A u = suc y))
4	1, 3	orbi12d 706	. . . . . 6 ⊢ (x = u → ((x = ∅ ∨ ∃y ∈ A x = suc y) ↔ (u = ∅ ∨ ∃y ∈ A u = suc y)))
5	4	rspcv 2646	. . . . 5 ⊢ (u ∈ A → (∀x ∈ A (x = ∅ ∨ ∃y ∈ A x = suc y) → (u = ∅ ∨ ∃y ∈ A u = suc y)))
6		df-bj-ind 9386	. . . . . . . . 9 ⊢ (Ind 𝑍 ↔ (∅ ∈ 𝑍 ∧ ∀v ∈ 𝑍 suc v ∈ 𝑍))
7	6	simplbi 259	. . . . . . . 8 ⊢ (Ind 𝑍 → ∅ ∈ 𝑍)
8		eleq1 2097	. . . . . . . 8 ⊢ (u = ∅ → (u ∈ 𝑍 ↔ ∅ ∈ 𝑍))
9	7, 8	syl5ibr 145	. . . . . . 7 ⊢ (u = ∅ → (Ind 𝑍 → u ∈ 𝑍))
10	9	a1dd 42	. . . . . 6 ⊢ (u = ∅ → (Ind 𝑍 → (∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → u ∈ 𝑍)))
11		vex 2554	. . . . . . . . . 10 ⊢ y ∈ V
12	11	sucid 4120	. . . . . . . . 9 ⊢ y ∈ suc y
13		eleq2 2098	. . . . . . . . . 10 ⊢ (suc y = u → (y ∈ suc y ↔ y ∈ u))
14	13	eqcoms 2040	. . . . . . . . 9 ⊢ (u = suc y → (y ∈ suc y ↔ y ∈ u))
15	12, 14	mpbii 136	. . . . . . . 8 ⊢ (u = suc y → y ∈ u)
16		eleq1 2097	. . . . . . . . . . . . 13 ⊢ (𝑡 = y → (𝑡 ∈ A ↔ y ∈ A))
17		eleq1 2097	. . . . . . . . . . . . 13 ⊢ (𝑡 = y → (𝑡 ∈ 𝑍 ↔ y ∈ 𝑍))
18	16, 17	imbi12d 223	. . . . . . . . . . . 12 ⊢ (𝑡 = y → ((𝑡 ∈ A → 𝑡 ∈ 𝑍) ↔ (y ∈ A → y ∈ 𝑍)))
19	18	rspcv 2646	. . . . . . . . . . 11 ⊢ (y ∈ u → (∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → (y ∈ A → y ∈ 𝑍)))
20		bj-indsuc 9387	. . . . . . . . . . . 12 ⊢ (Ind 𝑍 → (y ∈ 𝑍 → suc y ∈ 𝑍))
21		eleq1a 2106	. . . . . . . . . . . 12 ⊢ (suc y ∈ 𝑍 → (u = suc y → u ∈ 𝑍))
22	20, 21	syl6com 31	. . . . . . . . . . 11 ⊢ (y ∈ 𝑍 → (Ind 𝑍 → (u = suc y → u ∈ 𝑍)))
23	19, 22	syl8 65	. . . . . . . . . 10 ⊢ (y ∈ u → (∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → (y ∈ A → (Ind 𝑍 → (u = suc y → u ∈ 𝑍)))))
24	23	com13 74	. . . . . . . . 9 ⊢ (y ∈ A → (∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → (y ∈ u → (Ind 𝑍 → (u = suc y → u ∈ 𝑍)))))
25	24	com25 85	. . . . . . . 8 ⊢ (y ∈ A → (u = suc y → (y ∈ u → (Ind 𝑍 → (∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → u ∈ 𝑍)))))
26	15, 25	mpdi 38	. . . . . . 7 ⊢ (y ∈ A → (u = suc y → (Ind 𝑍 → (∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → u ∈ 𝑍))))
27	26	rexlimiv 2421	. . . . . 6 ⊢ (∃y ∈ A u = suc y → (Ind 𝑍 → (∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → u ∈ 𝑍)))
28	10, 27	jaoi 635	. . . . 5 ⊢ ((u = ∅ ∨ ∃y ∈ A u = suc y) → (Ind 𝑍 → (∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → u ∈ 𝑍)))
29	5, 28	syl6 29	. . . 4 ⊢ (u ∈ A → (∀x ∈ A (x = ∅ ∨ ∃y ∈ A x = suc y) → (Ind 𝑍 → (∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → u ∈ 𝑍))))
30	29	com3l 75	. . 3 ⊢ (∀x ∈ A (x = ∅ ∨ ∃y ∈ A x = suc y) → (Ind 𝑍 → (u ∈ A → (∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → u ∈ 𝑍))))
31	30	alrimdv 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 ∈ A → u ∈ 𝑍)))
33	32	albii 1356	. 2 ⊢ (∀u(u ∈ A → (∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → u ∈ 𝑍)) ↔ ∀u(∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → (u ∈ A → u ∈ 𝑍)))
34	31, 33	syl6ib 150	1 ⊢ (∀x ∈ A (x = ∅ ∨ ∃y ∈ A x = suc y) → (Ind 𝑍 → ∀u(∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → (u ∈ A → u ∈ 𝑍))))

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 9385

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-bndl 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 9386

This theorem is referenced by:  bj-inf2vnlem3  9432  bj-inf2vnlem4  9433