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 5 fndmi ⊢ dom ⁡ F = On
7 4 6 sseqtri ⊢ F -1 x ⊆ On
8 1 2 3 dnnumch2 ⊢ φ → A ⊆ ran ⁡ F
9 8 sselda ⊢ φ ∧ x ∈ A → x ∈ ran ⁡ F
10 inisegn0 ⊢ x ∈ ran ⁡ F ↔ F -1 x ≠ ∅
11 9 10 sylib ⊢ φ ∧ x ∈ A → F -1 x ≠ ∅
12 oninton ⊢ F -1 x ⊆ On ∧ F -1 x ≠ ∅ → ⋂ F -1 x ∈ On
13 7 11 12 sylancr ⊢ φ ∧ x ∈ A → ⋂ F -1 x ∈ On
14 13 fmpttd ⊢ φ → x ∈ A ⟼ ⋂ F -1 x : A ⟶ On
15 1 2 3 dnnumch3lem ⊢ φ ∧ v ∈ A → x ∈ A ⟼ ⋂ F -1 x ⁡ v = ⋂ F -1 v
16 15 adantrr ⊢ φ ∧ v ∈ A ∧ w ∈ A → x ∈ A ⟼ ⋂ F -1 x ⁡ v = ⋂ F -1 v
17 1 2 3 dnnumch3lem ⊢ φ ∧ w ∈ A → x ∈ A ⟼ ⋂ F -1 x ⁡ w = ⋂ F -1 w
18 17 adantrl ⊢ φ ∧ v ∈ A ∧ w ∈ A → x ∈ A ⟼ ⋂ F -1 x ⁡ w = ⋂ F -1 w
19 16 18 eqeq12d ⊢ φ ∧ v ∈ A ∧ w ∈ A → x ∈ A ⟼ ⋂ F -1 x ⁡ v = x ∈ A ⟼ ⋂ F -1 x ⁡ w ↔ ⋂ F -1 v = ⋂ F -1 w
20 fveq2 ⊢ ⋂ F -1 v = ⋂ F -1 w → F ⁡ ⋂ F -1 v = F ⁡ ⋂ F -1 w
21 20 adantl ⊢ φ ∧ v ∈ A ∧ w ∈ A ∧ ⋂ F -1 v = ⋂ F -1 w → F ⁡ ⋂ F -1 v = F ⁡ ⋂ F -1 w
22 cnvimass ⊢ F -1 v ⊆ dom ⁡ F
23 22 6 sseqtri ⊢ F -1 v ⊆ On
24 8 sselda ⊢ φ ∧ v ∈ A → v ∈ ran ⁡ F
25 inisegn0 ⊢ v ∈ ran ⁡ F ↔ F -1 v ≠ ∅
26 24 25 sylib ⊢ φ ∧ v ∈ A → F -1 v ≠ ∅
27 onint ⊢ F -1 v ⊆ On ∧ F -1 v ≠ ∅ → ⋂ F -1 v ∈ F -1 v
28 23 26 27 sylancr ⊢ φ ∧ v ∈ A → ⋂ F -1 v ∈ F -1 v
29 fniniseg ⊢ F Fn On → ⋂ F -1 v ∈ F -1 v ↔ ⋂ F -1 v ∈ On ∧ F ⁡ ⋂ F -1 v = v
30 5 29 ax-mp ⊢ ⋂ F -1 v ∈ F -1 v ↔ ⋂ F -1 v ∈ On ∧ F ⁡ ⋂ F -1 v = v
31 30 simprbi ⊢ ⋂ F -1 v ∈ F -1 v → F ⁡ ⋂ F -1 v = v
32 28 31 syl ⊢ φ ∧ v ∈ A → F ⁡ ⋂ F -1 v = v
33 32 adantrr ⊢ φ ∧ v ∈ A ∧ w ∈ A → F ⁡ ⋂ F -1 v = v
34 33 adantr ⊢ φ ∧ v ∈ A ∧ w ∈ A ∧ ⋂ F -1 v = ⋂ F -1 w → F ⁡ ⋂ F -1 v = v
35 cnvimass ⊢ F -1 w ⊆ dom ⁡ F
36 35 6 sseqtri ⊢ F -1 w ⊆ On
37 8 sselda ⊢ φ ∧ w ∈ A → w ∈ ran ⁡ F
38 inisegn0 ⊢ w ∈ ran ⁡ F ↔ F -1 w ≠ ∅
39 37 38 sylib ⊢ φ ∧ w ∈ A → F -1 w ≠ ∅
40 onint ⊢ F -1 w ⊆ On ∧ F -1 w ≠ ∅ → ⋂ F -1 w ∈ F -1 w
41 36 39 40 sylancr ⊢ φ ∧ w ∈ A → ⋂ F -1 w ∈ F -1 w
42 fniniseg ⊢ F Fn On → ⋂ F -1 w ∈ F -1 w ↔ ⋂ F -1 w ∈ On ∧ F ⁡ ⋂ F -1 w = w
43 5 42 ax-mp ⊢ ⋂ F -1 w ∈ F -1 w ↔ ⋂ F -1 w ∈ On ∧ F ⁡ ⋂ F -1 w = w
44 43 simprbi ⊢ ⋂ F -1 w ∈ F -1 w → F ⁡ ⋂ F -1 w = w
45 41 44 syl ⊢ φ ∧ w ∈ A → F ⁡ ⋂ F -1 w = w
46 45 adantrl ⊢ φ ∧ v ∈ A ∧ w ∈ A → F ⁡ ⋂ F -1 w = w
47 46 adantr ⊢ φ ∧ v ∈ A ∧ w ∈ A ∧ ⋂ F -1 v = ⋂ F -1 w → F ⁡ ⋂ F -1 w = w
48 21 34 47 3eqtr3d ⊢ φ ∧ v ∈ A ∧ w ∈ A ∧ ⋂ F -1 v = ⋂ F -1 w → v = w
49 48 ex ⊢ φ ∧ v ∈ A ∧ w ∈ A → ⋂ F -1 v = ⋂ F -1 w → v = w
50 19 49 sylbid ⊢ φ ∧ v ∈ A ∧ w ∈ A → x ∈ A ⟼ ⋂ F -1 x ⁡ v = x ∈ A ⟼ ⋂ F -1 x ⁡ w → v = w
51 50 ralrimivva ⊢ φ → ∀ v ∈ A ∀ w ∈ A x ∈ A ⟼ ⋂ F -1 x ⁡ v = x ∈ A ⟼ ⋂ F -1 x ⁡ w → v = w
52 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
53 14 51 52 sylanbrc ⊢ φ → x ∈ A ⟼ ⋂ F -1 x : A ⟶ 1-1 On