Step |
Hyp |
Ref |
Expression |
1 |
|
cantnfs.s |
⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 ) |
2 |
|
cantnfs.a |
⊢ ( 𝜑 → 𝐴 ∈ On ) |
3 |
|
cantnfs.b |
⊢ ( 𝜑 → 𝐵 ∈ On ) |
4 |
|
oemapval.t |
⊢ 𝑇 = { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } |
5 |
|
oemapval.f |
⊢ ( 𝜑 → 𝐹 ∈ 𝑆 ) |
6 |
|
oemapval.g |
⊢ ( 𝜑 → 𝐺 ∈ 𝑆 ) |
7 |
|
oemapvali.r |
⊢ ( 𝜑 → 𝐹 𝑇 𝐺 ) |
8 |
|
oemapvali.x |
⊢ 𝑋 = ∪ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } |
9 |
1 2 3 4 5 6 7 8
|
oemapvali |
⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐺 ‘ 𝑋 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) |
10 |
9
|
simp1d |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
11 |
9
|
simp2d |
⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐺 ‘ 𝑋 ) ) |
12 |
11
|
ne0d |
⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) |
13 |
1 2 3
|
cantnfs |
⊢ ( 𝜑 → ( 𝐺 ∈ 𝑆 ↔ ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐺 finSupp ∅ ) ) ) |
14 |
6 13
|
mpbid |
⊢ ( 𝜑 → ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐺 finSupp ∅ ) ) |
15 |
14
|
simpld |
⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 ) |
16 |
15
|
ffnd |
⊢ ( 𝜑 → 𝐺 Fn 𝐵 ) |
17 |
|
0ex |
⊢ ∅ ∈ V |
18 |
17
|
a1i |
⊢ ( 𝜑 → ∅ ∈ V ) |
19 |
|
elsuppfn |
⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V ) → ( 𝑋 ∈ ( 𝐺 supp ∅ ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) ) ) |
20 |
16 3 18 19
|
syl3anc |
⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐺 supp ∅ ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) ) ) |
21 |
10 12 20
|
mpbir2and |
⊢ ( 𝜑 → 𝑋 ∈ ( 𝐺 supp ∅ ) ) |