This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐺 = ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } )
inf3lem.2 ⊢ 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω )
inf3lem.3 ⊢ 𝐴 ∈ V
inf3lem.4 ⊢ 𝐵 ∈ V
Assertion inf3lem6 ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → 𝐹 : ω –1-1→ 𝒫 𝑥 )

Proof

Step Hyp Ref Expression
1 inf3lem.1 ⊢ 𝐺 = ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } )
2 inf3lem.2 ⊢ 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω )
3 inf3lem.3 ⊢ 𝐴 ∈ V
4 inf3lem.4 ⊢ 𝐵 ∈ V
5 vex ⊢ 𝑢 ∈ V
6 vex ⊢ 𝑣 ∈ V
7 1 2 5 6 inf3lem5 ⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( ( 𝑢 ∈ ω ∧ 𝑣 ∈ 𝑢 ) → ( 𝐹 ‘ 𝑣 ) ⊊ ( 𝐹 ‘ 𝑢 ) ) )
8 dfpss2 ⊢ ( ( 𝐹 ‘ 𝑣 ) ⊊ ( 𝐹 ‘ 𝑢 ) ↔ ( ( 𝐹 ‘ 𝑣 ) ⊆ ( 𝐹 ‘ 𝑢 ) ∧ ¬ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑢 ) ) )
9 8 simprbi ⊢ ( ( 𝐹 ‘ 𝑣 ) ⊊ ( 𝐹 ‘ 𝑢 ) → ¬ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑢 ) )
10 7 9 syl6 ⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( ( 𝑢 ∈ ω ∧ 𝑣 ∈ 𝑢 ) → ¬ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑢 ) ) )
11 10 expdimp ⊢ ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) ∧ 𝑢 ∈ ω ) → ( 𝑣 ∈ 𝑢 → ¬ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑢 ) ) )
12 11 adantrl ⊢ ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) ∧ ( 𝑣 ∈ ω ∧ 𝑢 ∈ ω ) ) → ( 𝑣 ∈ 𝑢 → ¬ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑢 ) ) )
13 1 2 6 5 inf3lem5 ⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( ( 𝑣 ∈ ω ∧ 𝑢 ∈ 𝑣 ) → ( 𝐹 ‘ 𝑢 ) ⊊ ( 𝐹 ‘ 𝑣 ) ) )
14 dfpss2 ⊢ ( ( 𝐹 ‘ 𝑢 ) ⊊ ( 𝐹 ‘ 𝑣 ) ↔ ( ( 𝐹 ‘ 𝑢 ) ⊆ ( 𝐹 ‘ 𝑣 ) ∧ ¬ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ) )
15 14 simprbi ⊢ ( ( 𝐹 ‘ 𝑢 ) ⊊ ( 𝐹 ‘ 𝑣 ) → ¬ ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) )
16 eqcom ⊢ ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) ↔ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑢 ) )
17 15 16 sylnib ⊢ ( ( 𝐹 ‘ 𝑢 ) ⊊ ( 𝐹 ‘ 𝑣 ) → ¬ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑢 ) )
18 13 17 syl6 ⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( ( 𝑣 ∈ ω ∧ 𝑢 ∈ 𝑣 ) → ¬ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑢 ) ) )
19 18 expdimp ⊢ ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) ∧ 𝑣 ∈ ω ) → ( 𝑢 ∈ 𝑣 → ¬ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑢 ) ) )
20 19 adantrr ⊢ ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) ∧ ( 𝑣 ∈ ω ∧ 𝑢 ∈ ω ) ) → ( 𝑢 ∈ 𝑣 → ¬ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑢 ) ) )
21 12 20 jaod ⊢ ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) ∧ ( 𝑣 ∈ ω ∧ 𝑢 ∈ ω ) ) → ( ( 𝑣 ∈ 𝑢 ∨ 𝑢 ∈ 𝑣 ) → ¬ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑢 ) ) )
22 21 con2d ⊢ ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) ∧ ( 𝑣 ∈ ω ∧ 𝑢 ∈ ω ) ) → ( ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑢 ) → ¬ ( 𝑣 ∈ 𝑢 ∨ 𝑢 ∈ 𝑣 ) ) )
23 nnord ⊢ ( 𝑣 ∈ ω → Ord 𝑣 )
24 nnord ⊢ ( 𝑢 ∈ ω → Ord 𝑢 )
25 ordtri3 ⊢ ( ( Ord 𝑣 ∧ Ord 𝑢 ) → ( 𝑣 = 𝑢 ↔ ¬ ( 𝑣 ∈ 𝑢 ∨ 𝑢 ∈ 𝑣 ) ) )
26 23 24 25 syl2an ⊢ ( ( 𝑣 ∈ ω ∧ 𝑢 ∈ ω ) → ( 𝑣 = 𝑢 ↔ ¬ ( 𝑣 ∈ 𝑢 ∨ 𝑢 ∈ 𝑣 ) ) )
27 26 adantl ⊢ ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) ∧ ( 𝑣 ∈ ω ∧ 𝑢 ∈ ω ) ) → ( 𝑣 = 𝑢 ↔ ¬ ( 𝑣 ∈ 𝑢 ∨ 𝑢 ∈ 𝑣 ) ) )
28 22 27 sylibrd ⊢ ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) ∧ ( 𝑣 ∈ ω ∧ 𝑢 ∈ ω ) ) → ( ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑢 ) → 𝑣 = 𝑢 ) )
29 28 ralrimivva ⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ∀ 𝑣 ∈ ω ∀ 𝑢 ∈ ω ( ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑢 ) → 𝑣 = 𝑢 ) )
30 frfnom ⊢ ( rec ( 𝐺 , ∅ ) ↾ ω ) Fn ω
31 fneq1 ⊢ ( 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω ) → ( 𝐹 Fn ω ↔ ( rec ( 𝐺 , ∅ ) ↾ ω ) Fn ω ) )
32 30 31 mpbiri ⊢ ( 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω ) → 𝐹 Fn ω )
33 fvelrnb ⊢ ( 𝐹 Fn ω → ( 𝑢 ∈ ran 𝐹 ↔ ∃ 𝑣 ∈ ω ( 𝐹 ‘ 𝑣 ) = 𝑢 ) )
34 1 2 6 4 inf3lemd ⊢ ( 𝑣 ∈ ω → ( 𝐹 ‘ 𝑣 ) ⊆ 𝑥 )
35 fvex ⊢ ( 𝐹 ‘ 𝑣 ) ∈ V
36 35 elpw ⊢ ( ( 𝐹 ‘ 𝑣 ) ∈ 𝒫 𝑥 ↔ ( 𝐹 ‘ 𝑣 ) ⊆ 𝑥 )
37 34 36 sylibr ⊢ ( 𝑣 ∈ ω → ( 𝐹 ‘ 𝑣 ) ∈ 𝒫 𝑥 )
38 eleq1 ⊢ ( ( 𝐹 ‘ 𝑣 ) = 𝑢 → ( ( 𝐹 ‘ 𝑣 ) ∈ 𝒫 𝑥 ↔ 𝑢 ∈ 𝒫 𝑥 ) )
39 37 38 syl5ibcom ⊢ ( 𝑣 ∈ ω → ( ( 𝐹 ‘ 𝑣 ) = 𝑢 → 𝑢 ∈ 𝒫 𝑥 ) )
40 39 rexlimiv ⊢ ( ∃ 𝑣 ∈ ω ( 𝐹 ‘ 𝑣 ) = 𝑢 → 𝑢 ∈ 𝒫 𝑥 )
41 33 40 biimtrdi ⊢ ( 𝐹 Fn ω → ( 𝑢 ∈ ran 𝐹 → 𝑢 ∈ 𝒫 𝑥 ) )
42 41 ssrdv ⊢ ( 𝐹 Fn ω → ran 𝐹 ⊆ 𝒫 𝑥 )
43 42 ancli ⊢ ( 𝐹 Fn ω → ( 𝐹 Fn ω ∧ ran 𝐹 ⊆ 𝒫 𝑥 ) )
44 2 32 43 mp2b ⊢ ( 𝐹 Fn ω ∧ ran 𝐹 ⊆ 𝒫 𝑥 )
45 df-f ⊢ ( 𝐹 : ω ⟶ 𝒫 𝑥 ↔ ( 𝐹 Fn ω ∧ ran 𝐹 ⊆ 𝒫 𝑥 ) )
46 44 45 mpbir ⊢ 𝐹 : ω ⟶ 𝒫 𝑥
47 29 46 jctil ⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 : ω ⟶ 𝒫 𝑥 ∧ ∀ 𝑣 ∈ ω ∀ 𝑢 ∈ ω ( ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑢 ) → 𝑣 = 𝑢 ) ) )
48 dff13 ⊢ ( 𝐹 : ω –1-1→ 𝒫 𝑥 ↔ ( 𝐹 : ω ⟶ 𝒫 𝑥 ∧ ∀ 𝑣 ∈ ω ∀ 𝑢 ∈ ω ( ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑢 ) → 𝑣 = 𝑢 ) ) )
49 47 48 sylibr ⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → 𝐹 : ω –1-1→ 𝒫 𝑥 )