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

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 ⊢ 𝐹 = recs ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) )
dnnumch.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
dnnumch.g ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝐺 ‘ 𝑦 ) ∈ 𝑦 ) )
Assertion dnnumch3 ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) : 𝐴 –1-1→ On )

Proof

Step Hyp Ref Expression
1 dnnumch.f ⊢ 𝐹 = recs ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) )
2 dnnumch.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 dnnumch.g ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝐺 ‘ 𝑦 ) ∈ 𝑦 ) )
4 cnvimass ⊢ ( ◡ 𝐹 “ { 𝑥 } ) ⊆ dom 𝐹
5 1 tfr1 ⊢ 𝐹 Fn On
6 5 fndmi ⊢ dom 𝐹 = On
7 4 6 sseqtri ⊢ ( ◡ 𝐹 “ { 𝑥 } ) ⊆ On
8 1 2 3 dnnumch2 ⊢ ( 𝜑 → 𝐴 ⊆ ran 𝐹 )
9 8 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ran 𝐹 )
10 inisegn0 ⊢ ( 𝑥 ∈ ran 𝐹 ↔ ( ◡ 𝐹 “ { 𝑥 } ) ≠ ∅ )
11 9 10 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ◡ 𝐹 “ { 𝑥 } ) ≠ ∅ )
12 oninton ⊢ ( ( ( ◡ 𝐹 “ { 𝑥 } ) ⊆ On ∧ ( ◡ 𝐹 “ { 𝑥 } ) ≠ ∅ ) → ∩ ( ◡ 𝐹 “ { 𝑥 } ) ∈ On )
13 7 11 12 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∩ ( ◡ 𝐹 “ { 𝑥 } ) ∈ On )
14 13 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) : 𝐴 ⟶ On )
15 1 2 3 dnnumch3lem ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) = ∩ ( ◡ 𝐹 “ { 𝑣 } ) )
16 15 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) = ∩ ( ◡ 𝐹 “ { 𝑣 } ) )
17 1 2 3 dnnumch3lem ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) )
18 17 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) )
19 16 18 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) = ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) ↔ ∩ ( ◡ 𝐹 “ { 𝑣 } ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) )
20 fveq2 ⊢ ( ∩ ( ◡ 𝐹 “ { 𝑣 } ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) → ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ) = ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) )
21 20 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ∩ ( ◡ 𝐹 “ { 𝑣 } ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) → ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ) = ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) )
22 cnvimass ⊢ ( ◡ 𝐹 “ { 𝑣 } ) ⊆ dom 𝐹
23 22 6 sseqtri ⊢ ( ◡ 𝐹 “ { 𝑣 } ) ⊆ On
24 8 sselda ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → 𝑣 ∈ ran 𝐹 )
25 inisegn0 ⊢ ( 𝑣 ∈ ran 𝐹 ↔ ( ◡ 𝐹 “ { 𝑣 } ) ≠ ∅ )
26 24 25 sylib ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( ◡ 𝐹 “ { 𝑣 } ) ≠ ∅ )
27 onint ⊢ ( ( ( ◡ 𝐹 “ { 𝑣 } ) ⊆ On ∧ ( ◡ 𝐹 “ { 𝑣 } ) ≠ ∅ ) → ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ ( ◡ 𝐹 “ { 𝑣 } ) )
28 23 26 27 sylancr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ ( ◡ 𝐹 “ { 𝑣 } ) )
29 fniniseg ⊢ ( 𝐹 Fn On → ( ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ ( ◡ 𝐹 “ { 𝑣 } ) ↔ ( ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ On ∧ ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ) = 𝑣 ) ) )
30 5 29 ax-mp ⊢ ( ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ ( ◡ 𝐹 “ { 𝑣 } ) ↔ ( ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ On ∧ ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ) = 𝑣 ) )
31 30 simprbi ⊢ ( ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ ( ◡ 𝐹 “ { 𝑣 } ) → ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ) = 𝑣 )
32 28 31 syl ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ) = 𝑣 )
33 32 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ) = 𝑣 )
34 33 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ∩ ( ◡ 𝐹 “ { 𝑣 } ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) → ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ) = 𝑣 )
35 cnvimass ⊢ ( ◡ 𝐹 “ { 𝑤 } ) ⊆ dom 𝐹
36 35 6 sseqtri ⊢ ( ◡ 𝐹 “ { 𝑤 } ) ⊆ On
37 8 sselda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → 𝑤 ∈ ran 𝐹 )
38 inisegn0 ⊢ ( 𝑤 ∈ ran 𝐹 ↔ ( ◡ 𝐹 “ { 𝑤 } ) ≠ ∅ )
39 37 38 sylib ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ◡ 𝐹 “ { 𝑤 } ) ≠ ∅ )
40 onint ⊢ ( ( ( ◡ 𝐹 “ { 𝑤 } ) ⊆ On ∧ ( ◡ 𝐹 “ { 𝑤 } ) ≠ ∅ ) → ∩ ( ◡ 𝐹 “ { 𝑤 } ) ∈ ( ◡ 𝐹 “ { 𝑤 } ) )
41 36 39 40 sylancr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ∩ ( ◡ 𝐹 “ { 𝑤 } ) ∈ ( ◡ 𝐹 “ { 𝑤 } ) )
42 fniniseg ⊢ ( 𝐹 Fn On → ( ∩ ( ◡ 𝐹 “ { 𝑤 } ) ∈ ( ◡ 𝐹 “ { 𝑤 } ) ↔ ( ∩ ( ◡ 𝐹 “ { 𝑤 } ) ∈ On ∧ ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) = 𝑤 ) ) )
43 5 42 ax-mp ⊢ ( ∩ ( ◡ 𝐹 “ { 𝑤 } ) ∈ ( ◡ 𝐹 “ { 𝑤 } ) ↔ ( ∩ ( ◡ 𝐹 “ { 𝑤 } ) ∈ On ∧ ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) = 𝑤 ) )
44 43 simprbi ⊢ ( ∩ ( ◡ 𝐹 “ { 𝑤 } ) ∈ ( ◡ 𝐹 “ { 𝑤 } ) → ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) = 𝑤 )
45 41 44 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) = 𝑤 )
46 45 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) = 𝑤 )
47 46 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ∩ ( ◡ 𝐹 “ { 𝑣 } ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) → ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) = 𝑤 )
48 21 34 47 3eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ∩ ( ◡ 𝐹 “ { 𝑣 } ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) → 𝑣 = 𝑤 )
49 48 ex ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ∩ ( ◡ 𝐹 “ { 𝑣 } ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) → 𝑣 = 𝑤 ) )
50 19 49 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) = ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) → 𝑣 = 𝑤 ) )
51 50 ralrimivva ⊢ ( 𝜑 → ∀ 𝑣 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) = ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) → 𝑣 = 𝑤 ) )
52 dff13 ⊢ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) : 𝐴 –1-1→ On ↔ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) : 𝐴 ⟶ On ∧ ∀ 𝑣 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) = ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) → 𝑣 = 𝑤 ) ) )
53 14 51 52 sylanbrc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) : 𝐴 –1-1→ On )