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 fndm ( 𝐹 Fn On → dom 𝐹 = On )
7 5 6 ax-mp dom 𝐹 = On
8 4 7 sseqtri ( 𝐹 “ { 𝑥 } ) ⊆ On
9 1 2 3 dnnumch2 ( 𝜑𝐴 ⊆ ran 𝐹 )
10 9 sselda ( ( 𝜑𝑥𝐴 ) → 𝑥 ∈ ran 𝐹 )
11 inisegn0 ( 𝑥 ∈ ran 𝐹 ↔ ( 𝐹 “ { 𝑥 } ) ≠ ∅ )
12 10 11 sylib ( ( 𝜑𝑥𝐴 ) → ( 𝐹 “ { 𝑥 } ) ≠ ∅ )
13 oninton ( ( ( 𝐹 “ { 𝑥 } ) ⊆ On ∧ ( 𝐹 “ { 𝑥 } ) ≠ ∅ ) → ( 𝐹 “ { 𝑥 } ) ∈ On )
14 8 12 13 sylancr ( ( 𝜑𝑥𝐴 ) → ( 𝐹 “ { 𝑥 } ) ∈ On )
15 14 fmpttd ( 𝜑 → ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) : 𝐴 ⟶ On )
16 1 2 3 dnnumch3lem ( ( 𝜑𝑣𝐴 ) → ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) = ( 𝐹 “ { 𝑣 } ) )
17 16 adantrr ( ( 𝜑 ∧ ( 𝑣𝐴𝑤𝐴 ) ) → ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) = ( 𝐹 “ { 𝑣 } ) )
18 1 2 3 dnnumch3lem ( ( 𝜑𝑤𝐴 ) → ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) = ( 𝐹 “ { 𝑤 } ) )
19 18 adantrl ( ( 𝜑 ∧ ( 𝑣𝐴𝑤𝐴 ) ) → ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) = ( 𝐹 “ { 𝑤 } ) )
20 17 19 eqeq12d ( ( 𝜑 ∧ ( 𝑣𝐴𝑤𝐴 ) ) → ( ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) = ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) ↔ ( 𝐹 “ { 𝑣 } ) = ( 𝐹 “ { 𝑤 } ) ) )
21 fveq2 ( ( 𝐹 “ { 𝑣 } ) = ( 𝐹 “ { 𝑤 } ) → ( 𝐹 ( 𝐹 “ { 𝑣 } ) ) = ( 𝐹 ( 𝐹 “ { 𝑤 } ) ) )
22 21 adantl ( ( ( 𝜑 ∧ ( 𝑣𝐴𝑤𝐴 ) ) ∧ ( 𝐹 “ { 𝑣 } ) = ( 𝐹 “ { 𝑤 } ) ) → ( 𝐹 ( 𝐹 “ { 𝑣 } ) ) = ( 𝐹 ( 𝐹 “ { 𝑤 } ) ) )
23 cnvimass ( 𝐹 “ { 𝑣 } ) ⊆ dom 𝐹
24 23 7 sseqtri ( 𝐹 “ { 𝑣 } ) ⊆ On
25 9 sselda ( ( 𝜑𝑣𝐴 ) → 𝑣 ∈ ran 𝐹 )
26 inisegn0 ( 𝑣 ∈ ran 𝐹 ↔ ( 𝐹 “ { 𝑣 } ) ≠ ∅ )
27 25 26 sylib ( ( 𝜑𝑣𝐴 ) → ( 𝐹 “ { 𝑣 } ) ≠ ∅ )
28 onint ( ( ( 𝐹 “ { 𝑣 } ) ⊆ On ∧ ( 𝐹 “ { 𝑣 } ) ≠ ∅ ) → ( 𝐹 “ { 𝑣 } ) ∈ ( 𝐹 “ { 𝑣 } ) )
29 24 27 28 sylancr ( ( 𝜑𝑣𝐴 ) → ( 𝐹 “ { 𝑣 } ) ∈ ( 𝐹 “ { 𝑣 } ) )
30 fniniseg ( 𝐹 Fn On → ( ( 𝐹 “ { 𝑣 } ) ∈ ( 𝐹 “ { 𝑣 } ) ↔ ( ( 𝐹 “ { 𝑣 } ) ∈ On ∧ ( 𝐹 ( 𝐹 “ { 𝑣 } ) ) = 𝑣 ) ) )
31 5 30 ax-mp ( ( 𝐹 “ { 𝑣 } ) ∈ ( 𝐹 “ { 𝑣 } ) ↔ ( ( 𝐹 “ { 𝑣 } ) ∈ On ∧ ( 𝐹 ( 𝐹 “ { 𝑣 } ) ) = 𝑣 ) )
32 31 simprbi ( ( 𝐹 “ { 𝑣 } ) ∈ ( 𝐹 “ { 𝑣 } ) → ( 𝐹 ( 𝐹 “ { 𝑣 } ) ) = 𝑣 )
33 29 32 syl ( ( 𝜑𝑣𝐴 ) → ( 𝐹 ( 𝐹 “ { 𝑣 } ) ) = 𝑣 )
34 33 adantrr ( ( 𝜑 ∧ ( 𝑣𝐴𝑤𝐴 ) ) → ( 𝐹 ( 𝐹 “ { 𝑣 } ) ) = 𝑣 )
35 34 adantr ( ( ( 𝜑 ∧ ( 𝑣𝐴𝑤𝐴 ) ) ∧ ( 𝐹 “ { 𝑣 } ) = ( 𝐹 “ { 𝑤 } ) ) → ( 𝐹 ( 𝐹 “ { 𝑣 } ) ) = 𝑣 )
36 cnvimass ( 𝐹 “ { 𝑤 } ) ⊆ dom 𝐹
37 36 7 sseqtri ( 𝐹 “ { 𝑤 } ) ⊆ On
38 9 sselda ( ( 𝜑𝑤𝐴 ) → 𝑤 ∈ ran 𝐹 )
39 inisegn0 ( 𝑤 ∈ ran 𝐹 ↔ ( 𝐹 “ { 𝑤 } ) ≠ ∅ )
40 38 39 sylib ( ( 𝜑𝑤𝐴 ) → ( 𝐹 “ { 𝑤 } ) ≠ ∅ )
41 onint ( ( ( 𝐹 “ { 𝑤 } ) ⊆ On ∧ ( 𝐹 “ { 𝑤 } ) ≠ ∅ ) → ( 𝐹 “ { 𝑤 } ) ∈ ( 𝐹 “ { 𝑤 } ) )
42 37 40 41 sylancr ( ( 𝜑𝑤𝐴 ) → ( 𝐹 “ { 𝑤 } ) ∈ ( 𝐹 “ { 𝑤 } ) )
43 fniniseg ( 𝐹 Fn On → ( ( 𝐹 “ { 𝑤 } ) ∈ ( 𝐹 “ { 𝑤 } ) ↔ ( ( 𝐹 “ { 𝑤 } ) ∈ On ∧ ( 𝐹 ( 𝐹 “ { 𝑤 } ) ) = 𝑤 ) ) )
44 5 43 ax-mp ( ( 𝐹 “ { 𝑤 } ) ∈ ( 𝐹 “ { 𝑤 } ) ↔ ( ( 𝐹 “ { 𝑤 } ) ∈ On ∧ ( 𝐹 ( 𝐹 “ { 𝑤 } ) ) = 𝑤 ) )
45 44 simprbi ( ( 𝐹 “ { 𝑤 } ) ∈ ( 𝐹 “ { 𝑤 } ) → ( 𝐹 ( 𝐹 “ { 𝑤 } ) ) = 𝑤 )
46 42 45 syl ( ( 𝜑𝑤𝐴 ) → ( 𝐹 ( 𝐹 “ { 𝑤 } ) ) = 𝑤 )
47 46 adantrl ( ( 𝜑 ∧ ( 𝑣𝐴𝑤𝐴 ) ) → ( 𝐹 ( 𝐹 “ { 𝑤 } ) ) = 𝑤 )
48 47 adantr ( ( ( 𝜑 ∧ ( 𝑣𝐴𝑤𝐴 ) ) ∧ ( 𝐹 “ { 𝑣 } ) = ( 𝐹 “ { 𝑤 } ) ) → ( 𝐹 ( 𝐹 “ { 𝑤 } ) ) = 𝑤 )
49 22 35 48 3eqtr3d ( ( ( 𝜑 ∧ ( 𝑣𝐴𝑤𝐴 ) ) ∧ ( 𝐹 “ { 𝑣 } ) = ( 𝐹 “ { 𝑤 } ) ) → 𝑣 = 𝑤 )
50 49 ex ( ( 𝜑 ∧ ( 𝑣𝐴𝑤𝐴 ) ) → ( ( 𝐹 “ { 𝑣 } ) = ( 𝐹 “ { 𝑤 } ) → 𝑣 = 𝑤 ) )
51 20 50 sylbid ( ( 𝜑 ∧ ( 𝑣𝐴𝑤𝐴 ) ) → ( ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) = ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) → 𝑣 = 𝑤 ) )
52 51 ralrimivva ( 𝜑 → ∀ 𝑣𝐴𝑤𝐴 ( ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) = ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) → 𝑣 = 𝑤 ) )
53 dff13 ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) : 𝐴1-1→ On ↔ ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) : 𝐴 ⟶ On ∧ ∀ 𝑣𝐴𝑤𝐴 ( ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) = ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) → 𝑣 = 𝑤 ) ) )
54 15 52 53 sylanbrc ( 𝜑 → ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) : 𝐴1-1→ On )