Metamath Proof Explorer

Theorem dnnumch1

Description: Define an enumeration of a set from a choice function; second part, it restricts to a bijection.EDITORIAL: overlaps dfac8a . (Contributed by Stefan O'Rear, 18-Jan-2015)

Ref Expression
Hypotheses dnnumch.f ⊢ 𝐹 = recs ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) )
dnnumch.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
dnnumch.g ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝐺 ‘ 𝑦 ) ∈ 𝑦 ) )
Assertion dnnumch1 ( 𝜑 → ∃ 𝑥 ∈ On ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝐴 )

Proof

Step Hyp Ref Expression
1 dnnumch.f ⊢ 𝐹 = recs ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) )
2 dnnumch.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 dnnumch.g ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝐺 ‘ 𝑦 ) ∈ 𝑦 ) )
4 recsval ⊢ ( 𝑥 ∈ On → ( recs ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) ) ‘ 𝑥 ) = ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) ‘ ( recs ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) ) ↾ 𝑥 ) ) )
5 1 fveq1i ⊢ ( 𝐹 ‘ 𝑥 ) = ( recs ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) ) ‘ 𝑥 )
6 1 tfr1 ⊢ 𝐹 Fn On
7 fnfun ⊢ ( 𝐹 Fn On → Fun 𝐹 )
8 6 7 ax-mp ⊢ Fun 𝐹
9 vex ⊢ 𝑥 ∈ V
10 resfunexg ⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ V ) → ( 𝐹 ↾ 𝑥 ) ∈ V )
11 8 9 10 mp2an ⊢ ( 𝐹 ↾ 𝑥 ) ∈ V
12 rneq ⊢ ( 𝑤 = ( 𝐹 ↾ 𝑥 ) → ran 𝑤 = ran ( 𝐹 ↾ 𝑥 ) )
13 df-ima ⊢ ( 𝐹 “ 𝑥 ) = ran ( 𝐹 ↾ 𝑥 )
14 12 13 eqtr4di ⊢ ( 𝑤 = ( 𝐹 ↾ 𝑥 ) → ran 𝑤 = ( 𝐹 “ 𝑥 ) )
15 14 difeq2d ⊢ ( 𝑤 = ( 𝐹 ↾ 𝑥 ) → ( 𝐴 ∖ ran 𝑤 ) = ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) )
16 15 fveq2d ⊢ ( 𝑤 = ( 𝐹 ↾ 𝑥 ) → ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑤 ) ) = ( 𝐺 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) )
17 rneq ⊢ ( 𝑧 = 𝑤 → ran 𝑧 = ran 𝑤 )
18 17 difeq2d ⊢ ( 𝑧 = 𝑤 → ( 𝐴 ∖ ran 𝑧 ) = ( 𝐴 ∖ ran 𝑤 ) )
19 18 fveq2d ⊢ ( 𝑧 = 𝑤 → ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) = ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑤 ) ) )
20 19 cbvmptv ⊢ ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) = ( 𝑤 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑤 ) ) )
21 fvex ⊢ ( 𝐺 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ∈ V
22 16 20 21 fvmpt ⊢ ( ( 𝐹 ↾ 𝑥 ) ∈ V → ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) ‘ ( 𝐹 ↾ 𝑥 ) ) = ( 𝐺 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) )
23 11 22 ax-mp ⊢ ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) ‘ ( 𝐹 ↾ 𝑥 ) ) = ( 𝐺 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) )
24 1 reseq1i ⊢ ( 𝐹 ↾ 𝑥 ) = ( recs ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) ) ↾ 𝑥 )
25 24 fveq2i ⊢ ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) ‘ ( 𝐹 ↾ 𝑥 ) ) = ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) ‘ ( recs ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) ) ↾ 𝑥 ) )
26 23 25 eqtr3i ⊢ ( 𝐺 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) = ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) ‘ ( recs ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) ) ↾ 𝑥 ) )
27 4 5 26 3eqtr4g ⊢ ( 𝑥 ∈ On → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) )
28 27 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ On ) ∧ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) )
29 difss ⊢ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ⊆ 𝐴
30 elpw2g ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ∈ 𝒫 𝐴 ↔ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ⊆ 𝐴 ) )
31 2 30 syl ⊢ ( 𝜑 → ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ∈ 𝒫 𝐴 ↔ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ⊆ 𝐴 ) )
32 29 31 mpbiri ⊢ ( 𝜑 → ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ∈ 𝒫 𝐴 )
33 neeq1 ⊢ ( 𝑦 = ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ( 𝑦 ≠ ∅ ↔ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ ) )
34 fveq2 ⊢ ( 𝑦 = ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) )
35 id ⊢ ( 𝑦 = ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → 𝑦 = ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) )
36 34 35 eleq12d ⊢ ( 𝑦 = ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑦 ↔ ( 𝐺 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) )
37 33 36 imbi12d ⊢ ( 𝑦 = ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ( ( 𝑦 ≠ ∅ → ( 𝐺 ‘ 𝑦 ) ∈ 𝑦 ) ↔ ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ → ( 𝐺 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ) )
38 37 rspcva ⊢ ( ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ∈ 𝒫 𝐴 ∧ ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝐺 ‘ 𝑦 ) ∈ 𝑦 ) ) → ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ → ( 𝐺 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) )
39 32 3 38 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ → ( 𝐺 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ On ) → ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ → ( 𝐺 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) )
41 40 imp ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ On ) ∧ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ ) → ( 𝐺 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) )
42 28 41 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ On ) ∧ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) )
43 42 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ On ) → ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) )
44 43 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) )
45 6 tz7.49c ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ) → ∃ 𝑥 ∈ On ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝐴 )
46 2 44 45 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ On ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝐴 )