Step | Hyp | Ref
| Expression |
1 | | pwexg 4850 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
2 | | rabexg 4812 |
. . . 4
⊢
(𝒫 𝐴 ∈
V → {𝑥 ∈
𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ∈ V) |
3 | | incom 3805 |
. . . . 5
⊢ ({𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ∩ On) = (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) |
4 | | inex1g 4801 |
. . . . 5
⊢ ({𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ∈ V → ({𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ∩ On) ∈ V) |
5 | 3, 4 | syl5eqelr 2706 |
. . . 4
⊢ ({𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ∈ V → (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ∈ V) |
6 | | inss1 3833 |
. . . . . . . . . . 11
⊢ (On ∩
{𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ⊆ On |
7 | 6 | sseli 3599 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) → 𝑧 ∈ On) |
8 | | onelon 5748 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → 𝑦 ∈ On) |
9 | 8 | ancoms 469 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ On) → 𝑦 ∈ On) |
10 | 7, 9 | sylan2 491 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴})) → 𝑦 ∈ On) |
11 | | onelss 5766 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ On → (𝑦 ∈ 𝑧 → 𝑦 ⊆ 𝑧)) |
12 | 11 | impcom 446 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ On) → 𝑦 ⊆ 𝑧) |
13 | 7, 12 | sylan2 491 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴})) → 𝑦 ⊆ 𝑧) |
14 | | inss2 3834 |
. . . . . . . . . . . . . . . . 17
⊢ (On ∩
{𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} |
15 | 14 | sseli 3599 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) → 𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) |
16 | | breq1 4656 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → (𝑥 ≺ 𝐴 ↔ 𝑧 ≺ 𝐴)) |
17 | 16 | elrab 3363 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ↔ (𝑧 ∈ 𝒫 𝐴 ∧ 𝑧 ≺ 𝐴)) |
18 | 15, 17 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) → (𝑧 ∈ 𝒫 𝐴 ∧ 𝑧 ≺ 𝐴)) |
19 | 18 | simpld 475 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) → 𝑧 ∈ 𝒫 𝐴) |
20 | 19 | elpwid 4170 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) → 𝑧 ⊆ 𝐴) |
21 | 20 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴})) → 𝑧 ⊆ 𝐴) |
22 | 13, 21 | sstrd 3613 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴})) → 𝑦 ⊆ 𝐴) |
23 | | selpw 4165 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴) |
24 | 22, 23 | sylibr 224 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴})) → 𝑦 ∈ 𝒫 𝐴) |
25 | | vex 3203 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ V |
26 | | ssdomg 8001 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ V → (𝑦 ⊆ 𝑧 → 𝑦 ≼ 𝑧)) |
27 | 25, 13, 26 | mpsyl 68 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴})) → 𝑦 ≼ 𝑧) |
28 | 18 | simprd 479 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) → 𝑧 ≺ 𝐴) |
29 | 28 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴})) → 𝑧 ≺ 𝐴) |
30 | | domsdomtr 8095 |
. . . . . . . . . . 11
⊢ ((𝑦 ≼ 𝑧 ∧ 𝑧 ≺ 𝐴) → 𝑦 ≺ 𝐴) |
31 | 27, 29, 30 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴})) → 𝑦 ≺ 𝐴) |
32 | | breq1 4656 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 ≺ 𝐴 ↔ 𝑦 ≺ 𝐴)) |
33 | 32 | elrab 3363 |
. . . . . . . . . 10
⊢ (𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ↔ (𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ≺ 𝐴)) |
34 | 24, 31, 33 | sylanbrc 698 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴})) → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) |
35 | 10, 34 | elind 3798 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴})) → 𝑦 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴})) |
36 | 35 | gen2 1723 |
. . . . . . 7
⊢
∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴})) → 𝑦 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴})) |
37 | | dftr2 4754 |
. . . . . . 7
⊢ (Tr (On
∩ {𝑥 ∈ 𝒫
𝐴 ∣ 𝑥 ≺ 𝐴}) ↔ ∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴})) → 𝑦 ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}))) |
38 | 36, 37 | mpbir 221 |
. . . . . 6
⊢ Tr (On
∩ {𝑥 ∈ 𝒫
𝐴 ∣ 𝑥 ≺ 𝐴}) |
39 | | ordon 6982 |
. . . . . 6
⊢ Ord
On |
40 | | trssord 5740 |
. . . . . 6
⊢ ((Tr (On
∩ {𝑥 ∈ 𝒫
𝐴 ∣ 𝑥 ≺ 𝐴}) ∧ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ⊆ On ∧ Ord On) → Ord (On
∩ {𝑥 ∈ 𝒫
𝐴 ∣ 𝑥 ≺ 𝐴})) |
41 | 38, 6, 39, 40 | mp3an 1424 |
. . . . 5
⊢ Ord (On
∩ {𝑥 ∈ 𝒫
𝐴 ∣ 𝑥 ≺ 𝐴}) |
42 | | elong 5731 |
. . . . 5
⊢ ((On
∩ {𝑥 ∈ 𝒫
𝐴 ∣ 𝑥 ≺ 𝐴}) ∈ V → ((On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ∈ On ↔ Ord (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}))) |
43 | 41, 42 | mpbiri 248 |
. . . 4
⊢ ((On
∩ {𝑥 ∈ 𝒫
𝐴 ∣ 𝑥 ≺ 𝐴}) ∈ V → (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ∈ On) |
44 | 1, 2, 5, 43 | 4syl 19 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ∈ On) |
45 | 44 | adantr 481 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ⊆ 𝐴) → (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ∈ On) |
46 | | simpr 477 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ⊆ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ⊆ 𝐴) |
47 | 14, 46 | syl5ss 3614 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ⊆ 𝐴) → (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ⊆ 𝐴) |
48 | | ssdomg 8001 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ((On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ⊆ 𝐴 → (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ≼ 𝐴)) |
49 | 48 | adantr 481 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ⊆ 𝐴) → ((On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ⊆ 𝐴 → (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ≼ 𝐴)) |
50 | 47, 49 | mpd 15 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ⊆ 𝐴) → (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ≼ 𝐴) |
51 | | ordirr 5741 |
. . . . 5
⊢ (Ord (On
∩ {𝑥 ∈ 𝒫
𝐴 ∣ 𝑥 ≺ 𝐴}) → ¬ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴})) |
52 | 41, 51 | mp1i 13 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ⊆ 𝐴) → ¬ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴})) |
53 | 44 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ⊆ 𝐴 ∧ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ≺ 𝐴) → (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ∈ On) |
54 | | elpw2g 4827 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → ((On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ∈ 𝒫 𝐴 ↔ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ⊆ 𝐴)) |
55 | 54 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ⊆ 𝐴) → ((On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ∈ 𝒫 𝐴 ↔ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ⊆ 𝐴)) |
56 | 47, 55 | mpbird 247 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ⊆ 𝐴) → (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ∈ 𝒫 𝐴) |
57 | 56 | 3adant3 1081 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ⊆ 𝐴 ∧ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ≺ 𝐴) → (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ∈ 𝒫 𝐴) |
58 | | simp3 1063 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ⊆ 𝐴 ∧ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ≺ 𝐴) → (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ≺ 𝐴) |
59 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑥On |
60 | | nfrab1 3122 |
. . . . . . . . 9
⊢
Ⅎ𝑥{𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} |
61 | 59, 60 | nfin 3820 |
. . . . . . . 8
⊢
Ⅎ𝑥(On
∩ {𝑥 ∈ 𝒫
𝐴 ∣ 𝑥 ≺ 𝐴}) |
62 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑥𝒫 𝐴 |
63 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑥
≺ |
64 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝐴 |
65 | 61, 63, 64 | nfbr 4699 |
. . . . . . . 8
⊢
Ⅎ𝑥(On ∩
{𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ≺ 𝐴 |
66 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑥 = (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) → (𝑥 ≺ 𝐴 ↔ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ≺ 𝐴)) |
67 | 61, 62, 65, 66 | elrabf 3360 |
. . . . . . 7
⊢ ((On
∩ {𝑥 ∈ 𝒫
𝐴 ∣ 𝑥 ≺ 𝐴}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ↔ ((On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ∈ 𝒫 𝐴 ∧ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ≺ 𝐴)) |
68 | 57, 58, 67 | sylanbrc 698 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ⊆ 𝐴 ∧ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ≺ 𝐴) → (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) |
69 | 53, 68 | elind 3798 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ⊆ 𝐴 ∧ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ≺ 𝐴) → (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴})) |
70 | 69 | 3expia 1267 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ⊆ 𝐴) → ((On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ≺ 𝐴 → (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ∈ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}))) |
71 | 52, 70 | mtod 189 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ⊆ 𝐴) → ¬ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ≺ 𝐴) |
72 | | bren2 7986 |
. . 3
⊢ ((On
∩ {𝑥 ∈ 𝒫
𝐴 ∣ 𝑥 ≺ 𝐴}) ≈ 𝐴 ↔ ((On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ≼ 𝐴 ∧ ¬ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ≺ 𝐴)) |
73 | 50, 71, 72 | sylanbrc 698 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ⊆ 𝐴) → (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ≈ 𝐴) |
74 | | isnumi 8772 |
. 2
⊢ (((On
∩ {𝑥 ∈ 𝒫
𝐴 ∣ 𝑥 ≺ 𝐴}) ∈ On ∧ (On ∩ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴}) ≈ 𝐴) → 𝐴 ∈ dom card) |
75 | 45, 73, 74 | syl2anc 693 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ⊆ 𝐴) → 𝐴 ∈ dom card) |