Theorem inf3lem3 9635

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9640 for detailed description. In the proof, we invoke the Axiom of Regularity in the form of zfreg 9594. (Contributed by NM, 29-Oct-1996.)

Hypotheses

Ref	Expression
inf3lem.1	⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})
inf3lem.2	⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)
inf3lem.3	⊢ 𝐴 ∈ V
inf3lem.4	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
inf3lem3	⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ≠ (𝐹‘suc 𝐴)))

Distinct variable group:   𝑥,𝑦,𝑤

Allowed substitution hints:   𝐴(𝑥, 𝑦, 𝑤)   𝐵(𝑥, 𝑦, 𝑤)   𝐹(𝑥, 𝑦, 𝑤)   𝐺(𝑥, 𝑦, 𝑤)

Proof of Theorem inf3lem3

Dummy variable 𝑣 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		inf3lem.1	. . . 4 ⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})
2		inf3lem.2	. . . 4 ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)
3		inf3lem.3	. . . 4 ⊢ 𝐴 ∈ V
4		inf3lem.4	. . . 4 ⊢ 𝐵 ∈ V
5	1, 2, 3, 4	inf3lemd 9632	. . 3 ⊢ (𝐴 ∈ ω → (𝐹‘𝐴) ⊆ 𝑥)
6	1, 2, 3, 4	inf3lem2 9634	. . . 4 ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ≠ 𝑥))
7	6	com12 33	. . 3 ⊢ (𝐴 ∈ ω → ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐹‘𝐴) ≠ 𝑥))
8		pssdifn0 4315	. . 3 ⊢ (((𝐹‘𝐴) ⊆ 𝑥 ∧ (𝐹‘𝐴) ≠ 𝑥) → (𝑥 ∖ (𝐹‘𝐴)) ≠ ∅)
9	5, 7, 8	syl6an 697	. 2 ⊢ (𝐴 ∈ ω → ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝑥 ∖ (𝐹‘𝐴)) ≠ ∅))
10		vex 3454	. . . . 5 ⊢ 𝑥 ∈ V
11	10	difexi 5291	. . . 4 ⊢ (𝑥 ∖ (𝐹‘𝐴)) ∈ V
12		zfreg 9594	. . . 4 ⊢ (((𝑥 ∖ (𝐹‘𝐴)) ∈ V ∧ (𝑥 ∖ (𝐹‘𝐴)) ≠ ∅) → ∃𝑣 ∈ (𝑥 ∖ (𝐹‘𝐴))(𝑣 ∩ (𝑥 ∖ (𝐹‘𝐴))) = ∅)
13	11, 12	mpan 703	. . 3 ⊢ ((𝑥 ∖ (𝐹‘𝐴)) ≠ ∅ → ∃𝑣 ∈ (𝑥 ∖ (𝐹‘𝐴))(𝑣 ∩ (𝑥 ∖ (𝐹‘𝐴))) = ∅)
14		eldifi 4067	. . . . . . . . . 10 ⊢ (𝑣 ∈ (𝑥 ∖ (𝐹‘𝐴)) → 𝑣 ∈ 𝑥)
15		inssdif0 4321	. . . . . . . . . . 11 ⊢ ((𝑣 ∩ 𝑥) ⊆ (𝐹‘𝐴) ↔ (𝑣 ∩ (𝑥 ∖ (𝐹‘𝐴))) = ∅)
16	15	biimpri 231	. . . . . . . . . 10 ⊢ ((𝑣 ∩ (𝑥 ∖ (𝐹‘𝐴))) = ∅ → (𝑣 ∩ 𝑥) ⊆ (𝐹‘𝐴))
17	14, 16	anim12i 625	. . . . . . . . 9 ⊢ ((𝑣 ∈ (𝑥 ∖ (𝐹‘𝐴)) ∧ (𝑣 ∩ (𝑥 ∖ (𝐹‘𝐴))) = ∅) → (𝑣 ∈ 𝑥 ∧ (𝑣 ∩ 𝑥) ⊆ (𝐹‘𝐴)))
18		vex 3454	. . . . . . . . . 10 ⊢ 𝑣 ∈ V
19		fvex 6899	. . . . . . . . . 10 ⊢ (𝐹‘𝐴) ∈ V
20	1, 2, 18, 19	inf3lema 9629	. . . . . . . . 9 ⊢ (𝑣 ∈ (𝐺‘(𝐹‘𝐴)) ↔ (𝑣 ∈ 𝑥 ∧ (𝑣 ∩ 𝑥) ⊆ (𝐹‘𝐴)))
21	17, 20	sylibr 237	. . . . . . . 8 ⊢ ((𝑣 ∈ (𝑥 ∖ (𝐹‘𝐴)) ∧ (𝑣 ∩ (𝑥 ∖ (𝐹‘𝐴))) = ∅) → 𝑣 ∈ (𝐺‘(𝐹‘𝐴)))
22	1, 2, 3, 4	inf3lemc 9631	. . . . . . . . 9 ⊢ (𝐴 ∈ ω → (𝐹‘suc 𝐴) = (𝐺‘(𝐹‘𝐴)))
23	22	eleq2d 2846	. . . . . . . 8 ⊢ (𝐴 ∈ ω → (𝑣 ∈ (𝐹‘suc 𝐴) ↔ 𝑣 ∈ (𝐺‘(𝐹‘𝐴))))
24	21, 23	imbitrrid 249	. . . . . . 7 ⊢ (𝐴 ∈ ω → ((𝑣 ∈ (𝑥 ∖ (𝐹‘𝐴)) ∧ (𝑣 ∩ (𝑥 ∖ (𝐹‘𝐴))) = ∅) → 𝑣 ∈ (𝐹‘suc 𝐴)))
25		eldifn 4068	. . . . . . . 8 ⊢ (𝑣 ∈ (𝑥 ∖ (𝐹‘𝐴)) → ¬ 𝑣 ∈ (𝐹‘𝐴))
26	25	adantr 486	. . . . . . 7 ⊢ ((𝑣 ∈ (𝑥 ∖ (𝐹‘𝐴)) ∧ (𝑣 ∩ (𝑥 ∖ (𝐹‘𝐴))) = ∅) → ¬ 𝑣 ∈ (𝐹‘𝐴))
27	24, 26	jca2 523	. . . . . 6 ⊢ (𝐴 ∈ ω → ((𝑣 ∈ (𝑥 ∖ (𝐹‘𝐴)) ∧ (𝑣 ∩ (𝑥 ∖ (𝐹‘𝐴))) = ∅) → (𝑣 ∈ (𝐹‘suc 𝐴) ∧ ¬ 𝑣 ∈ (𝐹‘𝐴))))
28		eleq2 2849	. . . . . . . . 9 ⊢ ((𝐹‘𝐴) = (𝐹‘suc 𝐴) → (𝑣 ∈ (𝐹‘𝐴) ↔ 𝑣 ∈ (𝐹‘suc 𝐴)))
29	28	biimprd 251	. . . . . . . 8 ⊢ ((𝐹‘𝐴) = (𝐹‘suc 𝐴) → (𝑣 ∈ (𝐹‘suc 𝐴) → 𝑣 ∈ (𝐹‘𝐴)))
30		iman 407	. . . . . . . 8 ⊢ ((𝑣 ∈ (𝐹‘suc 𝐴) → 𝑣 ∈ (𝐹‘𝐴)) ↔ ¬ (𝑣 ∈ (𝐹‘suc 𝐴) ∧ ¬ 𝑣 ∈ (𝐹‘𝐴)))
31	29, 30	sylib 221	. . . . . . 7 ⊢ ((𝐹‘𝐴) = (𝐹‘suc 𝐴) → ¬ (𝑣 ∈ (𝐹‘suc 𝐴) ∧ ¬ 𝑣 ∈ (𝐹‘𝐴)))
32	31	necon2ai 2984	. . . . . 6 ⊢ ((𝑣 ∈ (𝐹‘suc 𝐴) ∧ ¬ 𝑣 ∈ (𝐹‘𝐴)) → (𝐹‘𝐴) ≠ (𝐹‘suc 𝐴))
33	27, 32	syl6 36	. . . . 5 ⊢ (𝐴 ∈ ω → ((𝑣 ∈ (𝑥 ∖ (𝐹‘𝐴)) ∧ (𝑣 ∩ (𝑥 ∖ (𝐹‘𝐴))) = ∅) → (𝐹‘𝐴) ≠ (𝐹‘suc 𝐴)))
34	33	expd 421	. . . 4 ⊢ (𝐴 ∈ ω → (𝑣 ∈ (𝑥 ∖ (𝐹‘𝐴)) → ((𝑣 ∩ (𝑥 ∖ (𝐹‘𝐴))) = ∅ → (𝐹‘𝐴) ≠ (𝐹‘suc 𝐴))))
35	34	rexlimdv 3161	. . 3 ⊢ (𝐴 ∈ ω → (∃𝑣 ∈ (𝑥 ∖ (𝐹‘𝐴))(𝑣 ∩ (𝑥 ∖ (𝐹‘𝐴))) = ∅ → (𝐹‘𝐴) ≠ (𝐹‘suc 𝐴)))
36	13, 35	syl5 35	. 2 ⊢ (𝐴 ∈ ω → ((𝑥 ∖ (𝐹‘𝐴)) ≠ ∅ → (𝐹‘𝐴) ≠ (𝐹‘suc 𝐴)))
37	9, 36	syldc 49	1 ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ≠ (𝐹‘suc 𝐴)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144   ≠ wne 2955  ∃wrex 3086  {crab 3412  Vcvv 3450   ⊆ wss 3895   ∖ cdif 4045   ∩ cin 4089  ∅c0 4278  ∪ cuni 4866   ↦ cmpt 5185   ↾ cres 5652  suc csuc 6364  ‘cfv 6539  ωcom 7878  reccrdg 8421

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7752  ax-reg 9590

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-ov 7424  df-om 7879  df-2nd 8003  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-rdg 8422

This theorem is used by:  inf3lem4  9636