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 ) )