Step |
Hyp |
Ref |
Expression |
1 |
|
cantnfs.s |
⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 ) |
2 |
|
cantnfs.a |
⊢ ( 𝜑 → 𝐴 ∈ On ) |
3 |
|
cantnfs.b |
⊢ ( 𝜑 → 𝐵 ∈ On ) |
4 |
|
cantnfp1.g |
⊢ ( 𝜑 → 𝐺 ∈ 𝑆 ) |
5 |
|
cantnfp1.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
6 |
|
cantnfp1.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝐴 ) |
7 |
|
cantnfp1.s |
⊢ ( 𝜑 → ( 𝐺 supp ∅ ) ⊆ 𝑋 ) |
8 |
|
cantnfp1.f |
⊢ 𝐹 = ( 𝑡 ∈ 𝐵 ↦ if ( 𝑡 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑡 ) ) ) |
9 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → 𝑌 ∈ 𝐴 ) |
10 |
1 2 3
|
cantnfs |
⊢ ( 𝜑 → ( 𝐺 ∈ 𝑆 ↔ ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐺 finSupp ∅ ) ) ) |
11 |
4 10
|
mpbid |
⊢ ( 𝜑 → ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐺 finSupp ∅ ) ) |
12 |
11
|
simpld |
⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 ) |
13 |
12
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑡 ) ∈ 𝐴 ) |
14 |
9 13
|
ifcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → if ( 𝑡 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑡 ) ) ∈ 𝐴 ) |
15 |
14 8
|
fmptd |
⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐴 ) |
16 |
11
|
simprd |
⊢ ( 𝜑 → 𝐺 finSupp ∅ ) |
17 |
16
|
fsuppimpd |
⊢ ( 𝜑 → ( 𝐺 supp ∅ ) ∈ Fin ) |
18 |
|
snfi |
⊢ { 𝑋 } ∈ Fin |
19 |
|
unfi |
⊢ ( ( ( 𝐺 supp ∅ ) ∈ Fin ∧ { 𝑋 } ∈ Fin ) → ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ∈ Fin ) |
20 |
17 18 19
|
sylancl |
⊢ ( 𝜑 → ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ∈ Fin ) |
21 |
|
eqeq1 |
⊢ ( 𝑡 = 𝑘 → ( 𝑡 = 𝑋 ↔ 𝑘 = 𝑋 ) ) |
22 |
|
fveq2 |
⊢ ( 𝑡 = 𝑘 → ( 𝐺 ‘ 𝑡 ) = ( 𝐺 ‘ 𝑘 ) ) |
23 |
21 22
|
ifbieq2d |
⊢ ( 𝑡 = 𝑘 → if ( 𝑡 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑡 ) ) = if ( 𝑘 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑘 ) ) ) |
24 |
|
eldifi |
⊢ ( 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) → 𝑘 ∈ 𝐵 ) |
25 |
24
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) ) → 𝑘 ∈ 𝐵 ) |
26 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) ) → 𝑌 ∈ 𝐴 ) |
27 |
|
fvex |
⊢ ( 𝐺 ‘ 𝑘 ) ∈ V |
28 |
|
ifexg |
⊢ ( ( 𝑌 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑘 ) ∈ V ) → if ( 𝑘 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑘 ) ) ∈ V ) |
29 |
26 27 28
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) ) → if ( 𝑘 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑘 ) ) ∈ V ) |
30 |
8 23 25 29
|
fvmptd3 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑘 ) ) ) |
31 |
|
eldifn |
⊢ ( 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) → ¬ 𝑘 ∈ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) |
32 |
31
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) ) → ¬ 𝑘 ∈ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) |
33 |
|
velsn |
⊢ ( 𝑘 ∈ { 𝑋 } ↔ 𝑘 = 𝑋 ) |
34 |
|
elun2 |
⊢ ( 𝑘 ∈ { 𝑋 } → 𝑘 ∈ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) |
35 |
33 34
|
sylbir |
⊢ ( 𝑘 = 𝑋 → 𝑘 ∈ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) |
36 |
32 35
|
nsyl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) ) → ¬ 𝑘 = 𝑋 ) |
37 |
36
|
iffalsed |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) ) → if ( 𝑘 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑘 ) ) = ( 𝐺 ‘ 𝑘 ) ) |
38 |
|
ssun1 |
⊢ ( 𝐺 supp ∅ ) ⊆ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) |
39 |
|
sscon |
⊢ ( ( 𝐺 supp ∅ ) ⊆ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) → ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) ⊆ ( 𝐵 ∖ ( 𝐺 supp ∅ ) ) ) |
40 |
38 39
|
ax-mp |
⊢ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) ⊆ ( 𝐵 ∖ ( 𝐺 supp ∅ ) ) |
41 |
40
|
sseli |
⊢ ( 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) → 𝑘 ∈ ( 𝐵 ∖ ( 𝐺 supp ∅ ) ) ) |
42 |
|
ssidd |
⊢ ( 𝜑 → ( 𝐺 supp ∅ ) ⊆ ( 𝐺 supp ∅ ) ) |
43 |
|
0ex |
⊢ ∅ ∈ V |
44 |
43
|
a1i |
⊢ ( 𝜑 → ∅ ∈ V ) |
45 |
12 42 3 44
|
suppssr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( 𝐺 supp ∅ ) ) ) → ( 𝐺 ‘ 𝑘 ) = ∅ ) |
46 |
41 45
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) ) → ( 𝐺 ‘ 𝑘 ) = ∅ ) |
47 |
30 37 46
|
3eqtrd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) ) → ( 𝐹 ‘ 𝑘 ) = ∅ ) |
48 |
15 47
|
suppss |
⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ⊆ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) |
49 |
20 48
|
ssfid |
⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ∈ Fin ) |
50 |
8
|
funmpt2 |
⊢ Fun 𝐹 |
51 |
|
mptexg |
⊢ ( 𝐵 ∈ On → ( 𝑡 ∈ 𝐵 ↦ if ( 𝑡 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑡 ) ) ) ∈ V ) |
52 |
8 51
|
eqeltrid |
⊢ ( 𝐵 ∈ On → 𝐹 ∈ V ) |
53 |
3 52
|
syl |
⊢ ( 𝜑 → 𝐹 ∈ V ) |
54 |
|
funisfsupp |
⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ V ∧ ∅ ∈ V ) → ( 𝐹 finSupp ∅ ↔ ( 𝐹 supp ∅ ) ∈ Fin ) ) |
55 |
50 53 44 54
|
mp3an2i |
⊢ ( 𝜑 → ( 𝐹 finSupp ∅ ↔ ( 𝐹 supp ∅ ) ∈ Fin ) ) |
56 |
49 55
|
mpbird |
⊢ ( 𝜑 → 𝐹 finSupp ∅ ) |
57 |
1 2 3
|
cantnfs |
⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 : 𝐵 ⟶ 𝐴 ∧ 𝐹 finSupp ∅ ) ) ) |
58 |
15 56 57
|
mpbir2and |
⊢ ( 𝜑 → 𝐹 ∈ 𝑆 ) |