Theorem bj-inf2vnlem1 7384

Description: Lemma for bj-inf2vn 7388. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)

Assertion

Ref	Expression
bj-inf2vnlem1	⊢ (∀x(x ∈ A ↔ (x = ∅ ∨ ∃y ∈ A x = suc y)) → Ind A)

Distinct variable group:   x,A,y

Proof of Theorem bj-inf2vnlem1

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		bi2 121	. . . . 5 ⊢ ((x ∈ A ↔ (x = ∅ ∨ ∃y ∈ A x = suc y)) → ((x = ∅ ∨ ∃y ∈ A x = suc y) → x ∈ A))
2		ax-io 617	. . . . . 6 ⊢ (((x = ∅ ∨ ∃y ∈ A x = suc y) → x ∈ A) ↔ ((x = ∅ → x ∈ A) ∧ (∃y ∈ A x = suc y → x ∈ A)))
3	2	biimpi 113	. . . . 5 ⊢ (((x = ∅ ∨ ∃y ∈ A x = suc y) → x ∈ A) → ((x = ∅ → x ∈ A) ∧ (∃y ∈ A x = suc y → x ∈ A)))
4		ax-ia1 99	. . . . . 6 ⊢ (((x = ∅ → x ∈ A) ∧ (∃y ∈ A x = suc y → x ∈ A)) → (x = ∅ → x ∈ A))
5		eleq1 2078	. . . . . 6 ⊢ (x = ∅ → (x ∈ A ↔ ∅ ∈ A))
6	4, 5	mpbidi 140	. . . . 5 ⊢ (((x = ∅ → x ∈ A) ∧ (∃y ∈ A x = suc y → x ∈ A)) → (x = ∅ → ∅ ∈ A))
7	1, 3, 6	3syl 17	. . . 4 ⊢ ((x ∈ A ↔ (x = ∅ ∨ ∃y ∈ A x = suc y)) → (x = ∅ → ∅ ∈ A))
8	7	alimi 1320	. . 3 ⊢ (∀x(x ∈ A ↔ (x = ∅ ∨ ∃y ∈ A x = suc y)) → ∀x(x = ∅ → ∅ ∈ A))
9		exim 1468	. . 3 ⊢ (∀x(x = ∅ → ∅ ∈ A) → (∃x x = ∅ → ∃x∅ ∈ A))
10		0ex 3854	. . . . . 6 ⊢ ∅ ∈ V
11	10	isseti 2537	. . . . 5 ⊢ ∃x x = ∅
12		pm2.27 35	. . . . 5 ⊢ (∃x x = ∅ → ((∃x x = ∅ → ∃x∅ ∈ A) → ∃x∅ ∈ A))
13	11, 12	ax-mp 7	. . . 4 ⊢ ((∃x x = ∅ → ∃x∅ ∈ A) → ∃x∅ ∈ A)
14		bj-ex 7201	. . . 4 ⊢ (∃x∅ ∈ A → ∅ ∈ A)
15	13, 14	syl 14	. . 3 ⊢ ((∃x x = ∅ → ∃x∅ ∈ A) → ∅ ∈ A)
16	8, 9, 15	3syl 17	. 2 ⊢ (∀x(x ∈ A ↔ (x = ∅ ∨ ∃y ∈ A x = suc y)) → ∅ ∈ A)
17	3	simprd 107	. . . . . 6 ⊢ (((x = ∅ ∨ ∃y ∈ A x = suc y) → x ∈ A) → (∃y ∈ A x = suc y → x ∈ A))
18	1, 17	syl 14	. . . . 5 ⊢ ((x ∈ A ↔ (x = ∅ ∨ ∃y ∈ A x = suc y)) → (∃y ∈ A x = suc y → x ∈ A))
19	18	alimi 1320	. . . 4 ⊢ (∀x(x ∈ A ↔ (x = ∅ ∨ ∃y ∈ A x = suc y)) → ∀x(∃y ∈ A x = suc y → x ∈ A))
20		eqid 2018	. . . . 5 ⊢ suc z = suc z
21		suceq 4084	. . . . . . 7 ⊢ (y = z → suc y = suc z)
22	21	eqeq2d 2029	. . . . . 6 ⊢ (y = z → (suc z = suc y ↔ suc z = suc z))
23	22	rspcev 2629	. . . . 5 ⊢ ((z ∈ A ∧ suc z = suc z) → ∃y ∈ A suc z = suc y)
24	20, 23	mpan2 403	. . . 4 ⊢ (z ∈ A → ∃y ∈ A suc z = suc y)
25		vex 2534	. . . . . 6 ⊢ z ∈ V
26	25	bj-sucex 7338	. . . . 5 ⊢ suc z ∈ V
27		eqeq1 2024	. . . . . . 7 ⊢ (x = suc z → (x = suc y ↔ suc z = suc y))
28	27	rexbidv 2301	. . . . . 6 ⊢ (x = suc z → (∃y ∈ A x = suc y ↔ ∃y ∈ A suc z = suc y))
29		eleq1 2078	. . . . . 6 ⊢ (x = suc z → (x ∈ A ↔ suc z ∈ A))
30	28, 29	imbi12d 223	. . . . 5 ⊢ (x = suc z → ((∃y ∈ A x = suc y → x ∈ A) ↔ (∃y ∈ A suc z = suc y → suc z ∈ A)))
31	26, 30	spcv 2619	. . . 4 ⊢ (∀x(∃y ∈ A x = suc y → x ∈ A) → (∃y ∈ A suc z = suc y → suc z ∈ A))
32	19, 24, 31	syl2im 34	. . 3 ⊢ (∀x(x ∈ A ↔ (x = ∅ ∨ ∃y ∈ A x = suc y)) → (z ∈ A → suc z ∈ A))
33	32	ralrimiv 2365	. 2 ⊢ (∀x(x ∈ A ↔ (x = ∅ ∨ ∃y ∈ A x = suc y)) → ∀z ∈ A suc z ∈ A)
34		df-bj-ind 7346	. 2 ⊢ (Ind A ↔ (∅ ∈ A ∧ ∀z ∈ A suc z ∈ A))
35	16, 33, 34	sylanbrc 396	1 ⊢ (∀x(x ∈ A ↔ (x = ∅ ∨ ∃y ∈ A x = suc y)) → Ind A)

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 616  ∀wal 1224   = wceq 1226  ∃wex 1358   ∈ 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-in1 532  ax-in2 533  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-13 1381  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-nul 3853  ax-pr 3914  ax-un 4116  ax-bd0 7232  ax-bdor 7235  ax-bdex 7238  ax-bdeq 7239  ax-bdel 7240  ax-bdsb 7241  ax-bdsep 7303

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-dif 2893  df-un 2895  df-nul 3198  df-sn 3352  df-pr 3353  df-uni 3551  df-suc 4053  df-bdc 7260  df-bj-ind 7346

This theorem is referenced by:  bj-inf2vn  7388  bj-inf2vn2  7389