Metamath Proof Explorer

Theorem inf3lem6

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. (Contributed by NM, 29-Oct-1996)

Ref Expression
Hypotheses inf3lem.1 ⊢ G = y ∈ V ⟼ w ∈ x | w ∩ x ⊆ y
inf3lem.2 ⊢ F = rec ⁡ G ∅ ↾ ω
inf3lem.3 ⊢ A ∈ V
inf3lem.4 ⊢ B ∈ V
Assertion inf3lem6 ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x → F : ω ⟶ 1-1 𝒫 x

Proof

Step Hyp Ref Expression
1 inf3lem.1 ⊢ G = y ∈ V ⟼ w ∈ x | w ∩ x ⊆ y
2 inf3lem.2 ⊢ F = rec ⁡ G ∅ ↾ ω
3 inf3lem.3 ⊢ A ∈ V
4 inf3lem.4 ⊢ B ∈ V
5 vex ⊢ u ∈ V
6 vex ⊢ v ∈ V
7 1 2 5 6 inf3lem5 ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x → u ∈ ω ∧ v ∈ u → F ⁡ v ⊂ F ⁡ u
8 dfpss2 ⊢ F ⁡ v ⊂ F ⁡ u ↔ F ⁡ v ⊆ F ⁡ u ∧ ¬ F ⁡ v = F ⁡ u
9 8 simprbi ⊢ F ⁡ v ⊂ F ⁡ u → ¬ F ⁡ v = F ⁡ u
10 7 9 syl6 ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x → u ∈ ω ∧ v ∈ u → ¬ F ⁡ v = F ⁡ u
11 10 expdimp ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x ∧ u ∈ ω → v ∈ u → ¬ F ⁡ v = F ⁡ u
12 11 adantrl ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x ∧ v ∈ ω ∧ u ∈ ω → v ∈ u → ¬ F ⁡ v = F ⁡ u
13 1 2 6 5 inf3lem5 ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x → v ∈ ω ∧ u ∈ v → F ⁡ u ⊂ F ⁡ v
14 dfpss2 ⊢ F ⁡ u ⊂ F ⁡ v ↔ F ⁡ u ⊆ F ⁡ v ∧ ¬ F ⁡ u = F ⁡ v
15 14 simprbi ⊢ F ⁡ u ⊂ F ⁡ v → ¬ F ⁡ u = F ⁡ v
16 eqcom ⊢ F ⁡ u = F ⁡ v ↔ F ⁡ v = F ⁡ u
17 15 16 sylnib ⊢ F ⁡ u ⊂ F ⁡ v → ¬ F ⁡ v = F ⁡ u
18 13 17 syl6 ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x → v ∈ ω ∧ u ∈ v → ¬ F ⁡ v = F ⁡ u
19 18 expdimp ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x ∧ v ∈ ω → u ∈ v → ¬ F ⁡ v = F ⁡ u
20 19 adantrr ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x ∧ v ∈ ω ∧ u ∈ ω → u ∈ v → ¬ F ⁡ v = F ⁡ u
21 12 20 jaod ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x ∧ v ∈ ω ∧ u ∈ ω → v ∈ u ∨ u ∈ v → ¬ F ⁡ v = F ⁡ u
22 21 con2d ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x ∧ v ∈ ω ∧ u ∈ ω → F ⁡ v = F ⁡ u → ¬ v ∈ u ∨ u ∈ v
23 nnord ⊢ v ∈ ω → Ord ⁡ v
24 nnord ⊢ u ∈ ω → Ord ⁡ u
25 ordtri3 ⊢ Ord ⁡ v ∧ Ord ⁡ u → v = u ↔ ¬ v ∈ u ∨ u ∈ v
26 23 24 25 syl2an ⊢ v ∈ ω ∧ u ∈ ω → v = u ↔ ¬ v ∈ u ∨ u ∈ v
27 26 adantl ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x ∧ v ∈ ω ∧ u ∈ ω → v = u ↔ ¬ v ∈ u ∨ u ∈ v
28 22 27 sylibrd ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x ∧ v ∈ ω ∧ u ∈ ω → F ⁡ v = F ⁡ u → v = u
29 28 ralrimivva ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x → ∀ v ∈ ω ∀ u ∈ ω F ⁡ v = F ⁡ u → v = u
30 frfnom ⊢ rec ⁡ G ∅ ↾ ω Fn ω
31 fneq1 ⊢ F = rec ⁡ G ∅ ↾ ω → F Fn ω ↔ rec ⁡ G ∅ ↾ ω Fn ω
32 30 31 mpbiri ⊢ F = rec ⁡ G ∅ ↾ ω → F Fn ω
33 fvelrnb ⊢ F Fn ω → u ∈ ran ⁡ F ↔ ∃ v ∈ ω F ⁡ v = u
34 1 2 6 4 inf3lemd ⊢ v ∈ ω → F ⁡ v ⊆ x
35 fvex ⊢ F ⁡ v ∈ V
36 35 elpw ⊢ F ⁡ v ∈ 𝒫 x ↔ F ⁡ v ⊆ x
37 34 36 sylibr ⊢ v ∈ ω → F ⁡ v ∈ 𝒫 x
38 eleq1 ⊢ F ⁡ v = u → F ⁡ v ∈ 𝒫 x ↔ u ∈ 𝒫 x
39 37 38 syl5ibcom ⊢ v ∈ ω → F ⁡ v = u → u ∈ 𝒫 x
40 39 rexlimiv ⊢ ∃ v ∈ ω F ⁡ v = u → u ∈ 𝒫 x
41 33 40 syl6bi ⊢ F Fn ω → u ∈ ran ⁡ F → u ∈ 𝒫 x
42 41 ssrdv ⊢ F Fn ω → ran ⁡ F ⊆ 𝒫 x
43 42 ancli ⊢ F Fn ω → F Fn ω ∧ ran ⁡ F ⊆ 𝒫 x
44 2 32 43 mp2b ⊢ F Fn ω ∧ ran ⁡ F ⊆ 𝒫 x
45 df-f ⊢ F : ω ⟶ 𝒫 x ↔ F Fn ω ∧ ran ⁡ F ⊆ 𝒫 x
46 44 45 mpbir ⊢ F : ω ⟶ 𝒫 x
47 29 46 jctil ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x → F : ω ⟶ 𝒫 x ∧ ∀ v ∈ ω ∀ u ∈ ω F ⁡ v = F ⁡ u → v = u
48 dff13 ⊢ F : ω ⟶ 1-1 𝒫 x ↔ F : ω ⟶ 𝒫 x ∧ ∀ v ∈ ω ∀ u ∈ ω F ⁡ v = F ⁡ u → v = u
49 47 48 sylibr ⊢ x ≠ ∅ ∧ x ⊆ ⋃ x → F : ω ⟶ 1-1 𝒫 x