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

Metamath Proof Explorer

Theorem dfac8alem

Description: Lemma for dfac8a . If the power set of a set has a choice function, then the set is numerable. (Contributed by NM, 10-Feb-1997) (Revised by Mario Carneiro, 5-Jan-2013)

Ref Expression
Hypotheses dfac8alem.2 ⊢ 𝐹 = recs ( 𝐺 )
dfac8alem.3 ⊢ 𝐺 = ( 𝑓 ∈ V ↦ ( 𝑔 ‘ ( 𝐴 ∖ ran 𝑓 ) ) )
Assertion dfac8alem ( 𝐴 ∈ 𝐶 → ( ∃ 𝑔 ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) → 𝐴 ∈ dom card ) )

Proof

Step Hyp Ref Expression
1 dfac8alem.2 ⊢ 𝐹 = recs ( 𝐺 )
2 dfac8alem.3 ⊢ 𝐺 = ( 𝑓 ∈ V ↦ ( 𝑔 ‘ ( 𝐴 ∖ ran 𝑓 ) ) )
3 elex ⊢ ( 𝐴 ∈ 𝐶 → 𝐴 ∈ V )
4 difss ⊢ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ⊆ 𝐴
5 elpw2g ⊢ ( 𝐴 ∈ V → ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ∈ 𝒫 𝐴 ↔ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ⊆ 𝐴 ) )
6 4 5 mpbiri ⊢ ( 𝐴 ∈ V → ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ∈ 𝒫 𝐴 )
7 neeq1 ⊢ ( 𝑦 = ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ( 𝑦 ≠ ∅ ↔ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ ) )
8 fveq2 ⊢ ( 𝑦 = ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ( 𝑔 ‘ 𝑦 ) = ( 𝑔 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) )
9 id ⊢ ( 𝑦 = ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → 𝑦 = ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) )
10 8 9 eleq12d ⊢ ( 𝑦 = ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ( ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ↔ ( 𝑔 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) )
11 7 10 imbi12d ⊢ ( 𝑦 = ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ( ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ↔ ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ → ( 𝑔 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ) )
12 11 rspcv ⊢ ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ∈ 𝒫 𝐴 → ( ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) → ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ → ( 𝑔 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ) )
13 6 12 syl ⊢ ( 𝐴 ∈ V → ( ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) → ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ → ( 𝑔 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ) )
14 13 3imp ⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ ) → ( 𝑔 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) )
15 1 tfr2 ⊢ ( 𝑥 ∈ On → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝑥 ) ) )
16 1 tfr1 ⊢ 𝐹 Fn On
17 fnfun ⊢ ( 𝐹 Fn On → Fun 𝐹 )
18 16 17 ax-mp ⊢ Fun 𝐹
19 vex ⊢ 𝑥 ∈ V
20 resfunexg ⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ V ) → ( 𝐹 ↾ 𝑥 ) ∈ V )
21 18 19 20 mp2an ⊢ ( 𝐹 ↾ 𝑥 ) ∈ V
22 rneq ⊢ ( 𝑓 = ( 𝐹 ↾ 𝑥 ) → ran 𝑓 = ran ( 𝐹 ↾ 𝑥 ) )
23 df-ima ⊢ ( 𝐹 “ 𝑥 ) = ran ( 𝐹 ↾ 𝑥 )
24 22 23 eqtr4di ⊢ ( 𝑓 = ( 𝐹 ↾ 𝑥 ) → ran 𝑓 = ( 𝐹 “ 𝑥 ) )
25 24 difeq2d ⊢ ( 𝑓 = ( 𝐹 ↾ 𝑥 ) → ( 𝐴 ∖ ran 𝑓 ) = ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) )
26 25 fveq2d ⊢ ( 𝑓 = ( 𝐹 ↾ 𝑥 ) → ( 𝑔 ‘ ( 𝐴 ∖ ran 𝑓 ) ) = ( 𝑔 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) )
27 fvex ⊢ ( 𝑔 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ∈ V
28 26 2 27 fvmpt ⊢ ( ( 𝐹 ↾ 𝑥 ) ∈ V → ( 𝐺 ‘ ( 𝐹 ↾ 𝑥 ) ) = ( 𝑔 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) )
29 21 28 ax-mp ⊢ ( 𝐺 ‘ ( 𝐹 ↾ 𝑥 ) ) = ( 𝑔 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) )
30 15 29 eqtrdi ⊢ ( 𝑥 ∈ On → ( 𝐹 ‘ 𝑥 ) = ( 𝑔 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) )
31 30 eleq1d ⊢ ( 𝑥 ∈ On → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ↔ ( 𝑔 ‘ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) )
32 14 31 syl5ibrcom ⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ ) → ( 𝑥 ∈ On → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) )
33 32 3expia ⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ) → ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ → ( 𝑥 ∈ On → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ) )
34 33 com23 ⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ) → ( 𝑥 ∈ On → ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ) )
35 34 ralrimiv ⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ) → ∀ 𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) )
36 35 ex ⊢ ( 𝐴 ∈ V → ( ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) → ∀ 𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ) )
37 16 tz7.49c ⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ) → ∃ 𝑥 ∈ On ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝐴 )
38 37 ex ⊢ ( 𝐴 ∈ V → ( ∀ 𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) → ∃ 𝑥 ∈ On ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝐴 ) )
39 19 f1oen ⊢ ( ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝐴 → 𝑥 ≈ 𝐴 )
40 isnumi ⊢ ( ( 𝑥 ∈ On ∧ 𝑥 ≈ 𝐴 ) → 𝐴 ∈ dom card )
41 39 40 sylan2 ⊢ ( ( 𝑥 ∈ On ∧ ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝐴 ) → 𝐴 ∈ dom card )
42 41 rexlimiva ⊢ ( ∃ 𝑥 ∈ On ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝐴 → 𝐴 ∈ dom card )
43 38 42 syl6 ⊢ ( 𝐴 ∈ V → ( ∀ 𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) → 𝐴 ∈ dom card ) )
44 36 43 syld ⊢ ( 𝐴 ∈ V → ( ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) → 𝐴 ∈ dom card ) )
45 3 44 syl ⊢ ( 𝐴 ∈ 𝐶 → ( ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) → 𝐴 ∈ dom card ) )
46 45 exlimdv ⊢ ( 𝐴 ∈ 𝐶 → ( ∃ 𝑔 ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) → 𝐴 ∈ dom card ) )