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