Metamath Proof Explorer

Theorem dnnumch3

Description: Define an injection from a set into the ordinals using a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015)

Ref Expression
Hypotheses dnnumch.f ⊢ F = recs ⁡ z ∈ V ⟼ G ⁡ A ∖ ran ⁡ z
dnnumch.a ⊢ φ → A ∈ V
dnnumch.g ⊢ φ → ∀ y ∈ 𝒫 A y ≠ ∅ → G ⁡ y ∈ y
Assertion dnnumch3 ⊢ φ → x ∈ A ⟼ ⋂ F -1 x : A ⟶ 1-1 On

Proof

Step Hyp Ref Expression
1 dnnumch.f ⊢ F = recs ⁡ z ∈ V ⟼ G ⁡ A ∖ ran ⁡ z
2 dnnumch.a ⊢ φ → A ∈ V
3 dnnumch.g ⊢ φ → ∀ y ∈ 𝒫 A y ≠ ∅ → G ⁡ y ∈ y
4 cnvimass ⊢ F -1 x ⊆ dom ⁡ F
5 1 tfr1 ⊢ F Fn On
6 fndm ⊢ F Fn On → dom ⁡ F = On
7 5 6 ax-mp ⊢ dom ⁡ F = On
8 4 7 sseqtri ⊢ F -1 x ⊆ On
9 1 2 3 dnnumch2 ⊢ φ → A ⊆ ran ⁡ F
10 9 sselda ⊢ φ ∧ x ∈ A → x ∈ ran ⁡ F
11 inisegn0 ⊢ x ∈ ran ⁡ F ↔ F -1 x ≠ ∅
12 10 11 sylib ⊢ φ ∧ x ∈ A → F -1 x ≠ ∅
13 oninton ⊢ F -1 x ⊆ On ∧ F -1 x ≠ ∅ → ⋂ F -1 x ∈ On
14 8 12 13 sylancr ⊢ φ ∧ x ∈ A → ⋂ F -1 x ∈ On
15 14 fmpttd ⊢ φ → x ∈ A ⟼ ⋂ F -1 x : A ⟶ On
16 1 2 3 dnnumch3lem ⊢ φ ∧ v ∈ A → x ∈ A ⟼ ⋂ F -1 x ⁡ v = ⋂ F -1 v
17 16 adantrr ⊢ φ ∧ v ∈ A ∧ w ∈ A → x ∈ A ⟼ ⋂ F -1 x ⁡ v = ⋂ F -1 v
18 1 2 3 dnnumch3lem ⊢ φ ∧ w ∈ A → x ∈ A ⟼ ⋂ F -1 x ⁡ w = ⋂ F -1 w
19 18 adantrl ⊢ φ ∧ v ∈ A ∧ w ∈ A → x ∈ A ⟼ ⋂ F -1 x ⁡ w = ⋂ F -1 w
20 17 19 eqeq12d ⊢ φ ∧ v ∈ A ∧ w ∈ A → x ∈ A ⟼ ⋂ F -1 x ⁡ v = x ∈ A ⟼ ⋂ F -1 x ⁡ w ↔ ⋂ F -1 v = ⋂ F -1 w
21 fveq2 ⊢ ⋂ F -1 v = ⋂ F -1 w → F ⁡ ⋂ F -1 v = F ⁡ ⋂ F -1 w
22 21 adantl ⊢ φ ∧ v ∈ A ∧ w ∈ A ∧ ⋂ F -1 v = ⋂ F -1 w → F ⁡ ⋂ F -1 v = F ⁡ ⋂ F -1 w
23 cnvimass ⊢ F -1 v ⊆ dom ⁡ F
24 23 7 sseqtri ⊢ F -1 v ⊆ On
25 9 sselda ⊢ φ ∧ v ∈ A → v ∈ ran ⁡ F
26 inisegn0 ⊢ v ∈ ran ⁡ F ↔ F -1 v ≠ ∅
27 25 26 sylib ⊢ φ ∧ v ∈ A → F -1 v ≠ ∅
28 onint ⊢ F -1 v ⊆ On ∧ F -1 v ≠ ∅ → ⋂ F -1 v ∈ F -1 v
29 24 27 28 sylancr ⊢ φ ∧ v ∈ A → ⋂ F -1 v ∈ F -1 v
30 fniniseg ⊢ F Fn On → ⋂ F -1 v ∈ F -1 v ↔ ⋂ F -1 v ∈ On ∧ F ⁡ ⋂ F -1 v = v
31 5 30 ax-mp ⊢ ⋂ F -1 v ∈ F -1 v ↔ ⋂ F -1 v ∈ On ∧ F ⁡ ⋂ F -1 v = v
32 31 simprbi ⊢ ⋂ F -1 v ∈ F -1 v → F ⁡ ⋂ F -1 v = v
33 29 32 syl ⊢ φ ∧ v ∈ A → F ⁡ ⋂ F -1 v = v
34 33 adantrr ⊢ φ ∧ v ∈ A ∧ w ∈ A → F ⁡ ⋂ F -1 v = v
35 34 adantr ⊢ φ ∧ v ∈ A ∧ w ∈ A ∧ ⋂ F -1 v = ⋂ F -1 w → F ⁡ ⋂ F -1 v = v
36 cnvimass ⊢ F -1 w ⊆ dom ⁡ F
37 36 7 sseqtri ⊢ F -1 w ⊆ On
38 9 sselda ⊢ φ ∧ w ∈ A → w ∈ ran ⁡ F
39 inisegn0 ⊢ w ∈ ran ⁡ F ↔ F -1 w ≠ ∅
40 38 39 sylib ⊢ φ ∧ w ∈ A → F -1 w ≠ ∅
41 onint ⊢ F -1 w ⊆ On ∧ F -1 w ≠ ∅ → ⋂ F -1 w ∈ F -1 w
42 37 40 41 sylancr ⊢ φ ∧ w ∈ A → ⋂ F -1 w ∈ F -1 w
43 fniniseg ⊢ F Fn On → ⋂ F -1 w ∈ F -1 w ↔ ⋂ F -1 w ∈ On ∧ F ⁡ ⋂ F -1 w = w
44 5 43 ax-mp ⊢ ⋂ F -1 w ∈ F -1 w ↔ ⋂ F -1 w ∈ On ∧ F ⁡ ⋂ F -1 w = w
45 44 simprbi ⊢ ⋂ F -1 w ∈ F -1 w → F ⁡ ⋂ F -1 w = w
46 42 45 syl ⊢ φ ∧ w ∈ A → F ⁡ ⋂ F -1 w = w
47 46 adantrl ⊢ φ ∧ v ∈ A ∧ w ∈ A → F ⁡ ⋂ F -1 w = w
48 47 adantr ⊢ φ ∧ v ∈ A ∧ w ∈ A ∧ ⋂ F -1 v = ⋂ F -1 w → F ⁡ ⋂ F -1 w = w
49 22 35 48 3eqtr3d ⊢ φ ∧ v ∈ A ∧ w ∈ A ∧ ⋂ F -1 v = ⋂ F -1 w → v = w
50 49 ex ⊢ φ ∧ v ∈ A ∧ w ∈ A → ⋂ F -1 v = ⋂ F -1 w → v = w
51 20 50 sylbid ⊢ φ ∧ v ∈ A ∧ w ∈ A → x ∈ A ⟼ ⋂ F -1 x ⁡ v = x ∈ A ⟼ ⋂ F -1 x ⁡ w → v = w
52 51 ralrimivva ⊢ φ → ∀ v ∈ A ∀ w ∈ A x ∈ A ⟼ ⋂ F -1 x ⁡ v = x ∈ A ⟼ ⋂ F -1 x ⁡ w → v = w
53 dff13 ⊢ x ∈ A ⟼ ⋂ F -1 x : A ⟶ 1-1 On ↔ x ∈ A ⟼ ⋂ F -1 x : A ⟶ On ∧ ∀ v ∈ A ∀ w ∈ A x ∈ A ⟼ ⋂ F -1 x ⁡ v = x ∈ A ⟼ ⋂ F -1 x ⁡ w → v = w
54 15 52 53 sylanbrc ⊢ φ → x ∈ A ⟼ ⋂ F -1 x : A ⟶ 1-1 On