Step | Hyp | Ref
| Expression |
1 | | pwexg 5271 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
2 | | inex1g 5212 |
. . . 4
⊢
(𝒫 𝐴 ∈
V → (𝒫 𝐴 ∩
Fin) ∈ V) |
3 | | infpwfidom 9642 |
. . . 4
⊢
((𝒫 𝐴 ∩
Fin) ∈ V → 𝐴
≼ (𝒫 𝐴 ∩
Fin)) |
4 | 1, 2, 3 | 3syl 18 |
. . 3
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≼ (𝒫 𝐴 ∩ Fin)) |
5 | | inex1g 5212 |
. . . . 5
⊢
(𝒫 𝐴 ∈
V → (𝒫 𝐴 ∩
dom card) ∈ V) |
6 | 1, 5 | syl 17 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 ∩ dom card) ∈ V) |
7 | | finnum 9564 |
. . . . . 6
⊢ (𝑥 ∈ Fin → 𝑥 ∈ dom
card) |
8 | 7 | ssriv 3905 |
. . . . 5
⊢ Fin
⊆ dom card |
9 | | sslin 4149 |
. . . . 5
⊢ (Fin
⊆ dom card → (𝒫 𝐴 ∩ Fin) ⊆ (𝒫 𝐴 ∩ dom
card)) |
10 | 8, 9 | ax-mp 5 |
. . . 4
⊢
(𝒫 𝐴 ∩
Fin) ⊆ (𝒫 𝐴
∩ dom card) |
11 | | ssdomg 8674 |
. . . 4
⊢
((𝒫 𝐴 ∩
dom card) ∈ V → ((𝒫 𝐴 ∩ Fin) ⊆ (𝒫 𝐴 ∩ dom card) →
(𝒫 𝐴 ∩ Fin)
≼ (𝒫 𝐴 ∩
dom card))) |
12 | 6, 10, 11 | mpisyl 21 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 ∩ Fin) ≼ (𝒫 𝐴 ∩ dom
card)) |
13 | | domtr 8681 |
. . 3
⊢ ((𝐴 ≼ (𝒫 𝐴 ∩ Fin) ∧ (𝒫
𝐴 ∩ Fin) ≼
(𝒫 𝐴 ∩ dom
card)) → 𝐴 ≼
(𝒫 𝐴 ∩ dom
card)) |
14 | 4, 12, 13 | syl2anc 587 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≼ (𝒫 𝐴 ∩ dom card)) |
15 | | eqid 2737 |
. . . . . . 7
⊢
{〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘(◡𝑟 “ {𝑦})) = 𝑦))} = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘(◡𝑟 “ {𝑦})) = 𝑦))} |
16 | 15 | fpwwecbv 10258 |
. . . . . 6
⊢
{〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘(◡𝑟 “ {𝑦})) = 𝑦))} = {〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 (𝑓‘(◡𝑠 “ {𝑧})) = 𝑧))} |
17 | | eqid 2737 |
. . . . . 6
⊢ ∪ dom {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘(◡𝑟 “ {𝑦})) = 𝑦))} = ∪ dom
{〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘(◡𝑟 “ {𝑦})) = 𝑦))} |
18 | | eqid 2737 |
. . . . . 6
⊢ (◡({〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘(◡𝑟 “ {𝑦})) = 𝑦))}‘∪ dom
{〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘(◡𝑟 “ {𝑦})) = 𝑦))}) “ {(𝑓‘∪ dom
{〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘(◡𝑟 “ {𝑦})) = 𝑦))})}) = (◡({〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘(◡𝑟 “ {𝑦})) = 𝑦))}‘∪ dom
{〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘(◡𝑟 “ {𝑦})) = 𝑦))}) “ {(𝑓‘∪ dom
{〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘(◡𝑟 “ {𝑦})) = 𝑦))})}) |
19 | 16, 17, 18 | canthnumlem 10262 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ¬ 𝑓:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) |
20 | | f1of1 6660 |
. . . . 5
⊢ (𝑓:(𝒫 𝐴 ∩ dom card)–1-1-onto→𝐴 → 𝑓:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) |
21 | 19, 20 | nsyl 142 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ¬ 𝑓:(𝒫 𝐴 ∩ dom card)–1-1-onto→𝐴) |
22 | 21 | nexdv 1944 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ¬ ∃𝑓 𝑓:(𝒫 𝐴 ∩ dom card)–1-1-onto→𝐴) |
23 | | ensym 8677 |
. . . 4
⊢ (𝐴 ≈ (𝒫 𝐴 ∩ dom card) →
(𝒫 𝐴 ∩ dom
card) ≈ 𝐴) |
24 | | bren 8636 |
. . . 4
⊢
((𝒫 𝐴 ∩
dom card) ≈ 𝐴 ↔
∃𝑓 𝑓:(𝒫 𝐴 ∩ dom card)–1-1-onto→𝐴) |
25 | 23, 24 | sylib 221 |
. . 3
⊢ (𝐴 ≈ (𝒫 𝐴 ∩ dom card) →
∃𝑓 𝑓:(𝒫 𝐴 ∩ dom card)–1-1-onto→𝐴) |
26 | 22, 25 | nsyl 142 |
. 2
⊢ (𝐴 ∈ 𝑉 → ¬ 𝐴 ≈ (𝒫 𝐴 ∩ dom card)) |
27 | | brsdom 8651 |
. 2
⊢ (𝐴 ≺ (𝒫 𝐴 ∩ dom card) ↔ (𝐴 ≼ (𝒫 𝐴 ∩ dom card) ∧ ¬
𝐴 ≈ (𝒫 𝐴 ∩ dom
card))) |
28 | 14, 26, 27 | sylanbrc 586 |
1
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≺ (𝒫 𝐴 ∩ dom card)) |