Theorem bj-inf2vnlem1 9400

Description: Lemma for bj-inf2vn 9404. 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 629	. . . . . 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		simpl 102	. . . . . 6 ⊢ (((x = ∅ → x ∈ A) ∧ (∃y ∈ A x = suc y → x ∈ A)) → (x = ∅ → x ∈ A))
5		eleq1 2097	. . . . . 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 1341	. . 3 ⊢ (∀x(x ∈ A ↔ (x = ∅ ∨ ∃y ∈ A x = suc y)) → ∀x(x = ∅ → ∅ ∈ A))
9		exim 1487	. . 3 ⊢ (∀x(x = ∅ → ∅ ∈ A) → (∃x x = ∅ → ∃x∅ ∈ A))
10		0ex 3875	. . . . . 6 ⊢ ∅ ∈ V
11	10	isseti 2557	. . . . 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 9217	. . . 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 1341	. . . 4 ⊢ (∀x(x ∈ A ↔ (x = ∅ ∨ ∃y ∈ A x = suc y)) → ∀x(∃y ∈ A x = suc y → x ∈ A))
20		eqid 2037	. . . . 5 ⊢ suc z = suc z
21		suceq 4105	. . . . . . 7 ⊢ (y = z → suc y = suc z)
22	21	eqeq2d 2048	. . . . . 6 ⊢ (y = z → (suc z = suc y ↔ suc z = suc z))
23	22	rspcev 2650	. . . . 5 ⊢ ((z ∈ A ∧ suc z = suc z) → ∃y ∈ A suc z = suc y)
24	20, 23	mpan2 401	. . . 4 ⊢ (z ∈ A → ∃y ∈ A suc z = suc y)
25		vex 2554	. . . . . 6 ⊢ z ∈ V
26	25	bj-sucex 9354	. . . . 5 ⊢ suc z ∈ V
27		eqeq1 2043	. . . . . . 7 ⊢ (x = suc z → (x = suc y ↔ suc z = suc y))
28	27	rexbidv 2321	. . . . . 6 ⊢ (x = suc z → (∃y ∈ A x = suc y ↔ ∃y ∈ A suc z = suc y))
29		eleq1 2097	. . . . . 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 2640	. . . 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 2385	. 2 ⊢ (∀x(x ∈ A ↔ (x = ∅ ∨ ∃y ∈ A x = suc y)) → ∀z ∈ A suc z ∈ A)
34		df-bj-ind 9362	. 2 ⊢ (Ind A ↔ (∅ ∈ A ∧ ∀z ∈ A suc z ∈ A))
35	16, 33, 34	sylanbrc 394	1 ⊢ (∀x(x ∈ A ↔ (x = ∅ ∨ ∃y ∈ A x = suc y)) → Ind A)

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 628  ∀wal 1240   = wceq 1242  ∃wex 1378   ∈ 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-in1 544  ax-in2 545  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-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-nul 3874  ax-pr 3935  ax-un 4136  ax-bd0 9248  ax-bdor 9251  ax-bdex 9254  ax-bdeq 9255  ax-bdel 9256  ax-bdsb 9257  ax-bdsep 9319

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-dif 2914  df-un 2916  df-nul 3219  df-sn 3373  df-pr 3374  df-uni 3572  df-suc 4074  df-bdc 9276  df-bj-ind 9362

This theorem is referenced by:  bj-inf2vn  9404  bj-inf2vn2  9405