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 ∈ 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 2024	. . . . . . 7 ⊢ (x = u → (x = ∅ ↔ u = ∅))
2		eqeq1 2024	. . . . . . . 8 ⊢ (x = u → (x = suc y ↔ u = suc y))
3	2	rexbidv 2301	. . . . . . 7 ⊢ (x = u → (∃y ∈ A x = suc y ↔ ∃y ∈ A u = suc y))
4	1, 3	orbi12d 694	. . . . . 6 ⊢ (x = u → ((x = ∅ ∨ ∃y ∈ A x = suc y) ↔ (u = ∅ ∨ ∃y ∈ A u = suc y)))
5	4	rspcv 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 ∈ 𝑍))
7	6	simplbi 259	. . . . . . . 8 ⊢ (Ind 𝑍 → ∅ ∈ 𝑍)
8		eleq1 2078	. . . . . . . 8 ⊢ (u = ∅ → (u ∈ 𝑍 ↔ ∅ ∈ 𝑍))
9	7, 8	syl5ibr 145	. . . . . . 7 ⊢ (u = ∅ → (Ind 𝑍 → u ∈ 𝑍))
10	9	a1dd 42	. . . . . 6 ⊢ (u = ∅ → (Ind 𝑍 → (∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → u ∈ 𝑍)))
11		vex 2534	. . . . . . . . . 10 ⊢ y ∈ V
12	11	sucid 4099	. . . . . . . . 9 ⊢ y ∈ suc y
13		eleq2 2079	. . . . . . . . . 10 ⊢ (suc y = u → (y ∈ suc y ↔ y ∈ u))
14	13	eqcoms 2021	. . . . . . . . 9 ⊢ (u = suc y → (y ∈ suc y ↔ y ∈ u))
15	12, 14	mpbii 136	. . . . . . . 8 ⊢ (u = suc y → y ∈ u)
16		eleq1 2078	. . . . . . . . . . . . 13 ⊢ (𝑡 = y → (𝑡 ∈ A ↔ y ∈ A))
17		eleq1 2078	. . . . . . . . . . . . 13 ⊢ (𝑡 = y → (𝑡 ∈ 𝑍 ↔ y ∈ 𝑍))
18	16, 17	imbi12d 223	. . . . . . . . . . . 12 ⊢ (𝑡 = y → ((𝑡 ∈ A → 𝑡 ∈ 𝑍) ↔ (y ∈ A → y ∈ 𝑍)))
19	18	rspcv 2625	. . . . . . . . . . 11 ⊢ (y ∈ u → (∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → (y ∈ A → y ∈ 𝑍)))
20		bj-indsuc 7347	. . . . . . . . . . . 12 ⊢ (Ind 𝑍 → (y ∈ 𝑍 → suc y ∈ 𝑍))
21		eleq1a 2087	. . . . . . . . . . . 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 2401	. . . . . 6 ⊢ (∃y ∈ A u = suc y → (Ind 𝑍 → (∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → u ∈ 𝑍)))
28	10, 27	jaoi 623	. . . . 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 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 ∈ A → u ∈ 𝑍)))
33	32	albii 1335	. 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 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