Step | Hyp | Ref
| Expression |
1 | | porpss 6941 |
. . . 4
⊢
[⊊] Po 𝒫 𝐴 |
2 | | cnvpo 5673 |
. . . 4
⊢ (
[⊊] Po 𝒫 𝐴 ↔ ◡ [⊊] Po 𝒫 𝐴) |
3 | 1, 2 | mpbi 220 |
. . 3
⊢ ◡ [⊊] Po 𝒫 𝐴 |
4 | | pwfi 8261 |
. . . 4
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Fin) |
5 | 4 | biimpi 206 |
. . 3
⊢ (𝐴 ∈ Fin → 𝒫
𝐴 ∈
Fin) |
6 | | frfi 8205 |
. . 3
⊢ ((◡ [⊊] Po 𝒫 𝐴 ∧ 𝒫 𝐴 ∈ Fin) → ◡ [⊊] Fr 𝒫 𝐴) |
7 | 3, 5, 6 | sylancr 695 |
. 2
⊢ (𝐴 ∈ Fin → ◡ [⊊] Fr 𝒫 𝐴) |
8 | | inss2 3834 |
. . . . . 6
⊢ (Fin
∩ 𝒫 𝐴) ⊆
𝒫 𝐴 |
9 | | pwexg 4850 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
10 | | ssexg 4804 |
. . . . . 6
⊢ (((Fin
∩ 𝒫 𝐴) ⊆
𝒫 𝐴 ∧ 𝒫
𝐴 ∈ V) → (Fin
∩ 𝒫 𝐴) ∈
V) |
11 | 8, 9, 10 | sylancr 695 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (Fin ∩ 𝒫 𝐴) ∈ V) |
12 | | 0fin 8188 |
. . . . . . . 8
⊢ ∅
∈ Fin |
13 | | 0elpw 4834 |
. . . . . . . 8
⊢ ∅
∈ 𝒫 𝐴 |
14 | | elin 3796 |
. . . . . . . 8
⊢ (∅
∈ (Fin ∩ 𝒫 𝐴) ↔ (∅ ∈ Fin ∧ ∅
∈ 𝒫 𝐴)) |
15 | 12, 13, 14 | mpbir2an 955 |
. . . . . . 7
⊢ ∅
∈ (Fin ∩ 𝒫 𝐴) |
16 | 15 | ne0ii 3923 |
. . . . . 6
⊢ (Fin
∩ 𝒫 𝐴) ≠
∅ |
17 | | fri 5076 |
. . . . . 6
⊢ ((((Fin
∩ 𝒫 𝐴) ∈ V
∧ ◡ [⊊] Fr 𝒫
𝐴) ∧ ((Fin ∩
𝒫 𝐴) ⊆
𝒫 𝐴 ∧ (Fin
∩ 𝒫 𝐴) ≠
∅)) → ∃𝑏
∈ (Fin ∩ 𝒫 𝐴)∀𝑐 ∈ (Fin ∩ 𝒫 𝐴) ¬ 𝑐◡
[⊊] 𝑏) |
18 | 8, 16, 17 | mpanr12 721 |
. . . . 5
⊢ (((Fin
∩ 𝒫 𝐴) ∈ V
∧ ◡ [⊊] Fr 𝒫
𝐴) → ∃𝑏 ∈ (Fin ∩ 𝒫
𝐴)∀𝑐 ∈ (Fin ∩ 𝒫
𝐴) ¬ 𝑐◡
[⊊] 𝑏) |
19 | 11, 18 | sylan 488 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ◡ [⊊] Fr 𝒫 𝐴) → ∃𝑏 ∈ (Fin ∩ 𝒫
𝐴)∀𝑐 ∈ (Fin ∩ 𝒫
𝐴) ¬ 𝑐◡
[⊊] 𝑏) |
20 | 19 | ex 450 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (◡ [⊊] Fr 𝒫 𝐴 → ∃𝑏 ∈ (Fin ∩ 𝒫
𝐴)∀𝑐 ∈ (Fin ∩ 𝒫
𝐴) ¬ 𝑐◡
[⊊] 𝑏)) |
21 | | inss1 3833 |
. . . . . 6
⊢ (Fin
∩ 𝒫 𝐴) ⊆
Fin |
22 | | simpl 473 |
. . . . . 6
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ ∀𝑐 ∈ (Fin ∩ 𝒫
𝐴) ¬ 𝑐◡
[⊊] 𝑏) →
𝑏 ∈ (Fin ∩
𝒫 𝐴)) |
23 | 21, 22 | sseldi 3601 |
. . . . 5
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ ∀𝑐 ∈ (Fin ∩ 𝒫
𝐴) ¬ 𝑐◡
[⊊] 𝑏) →
𝑏 ∈
Fin) |
24 | | ralnex 2992 |
. . . . . . . 8
⊢
(∀𝑐 ∈
(Fin ∩ 𝒫 𝐴)
¬ 𝑐◡ [⊊] 𝑏 ↔ ¬ ∃𝑐 ∈ (Fin ∩ 𝒫 𝐴)𝑐◡
[⊊] 𝑏) |
25 | 21 | sseli 3599 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ (Fin ∩ 𝒫
𝐴) → 𝑏 ∈ Fin) |
26 | 25 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → 𝑏 ∈ Fin) |
27 | | snfi 8038 |
. . . . . . . . . . . . 13
⊢ {𝑑} ∈ Fin |
28 | | unfi 8227 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ Fin ∧ {𝑑} ∈ Fin) → (𝑏 ∪ {𝑑}) ∈ Fin) |
29 | 26, 27, 28 | sylancl 694 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → (𝑏 ∪ {𝑑}) ∈ Fin) |
30 | | elin 3796 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ (Fin ∩ 𝒫
𝐴) ↔ (𝑏 ∈ Fin ∧ 𝑏 ∈ 𝒫 𝐴)) |
31 | 30 | simprbi 480 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ (Fin ∩ 𝒫
𝐴) → 𝑏 ∈ 𝒫 𝐴) |
32 | 31 | elpwid 4170 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ (Fin ∩ 𝒫
𝐴) → 𝑏 ⊆ 𝐴) |
33 | 32 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → 𝑏 ⊆ 𝐴) |
34 | | snssi 4339 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 ∈ 𝐴 → {𝑑} ⊆ 𝐴) |
35 | 34 | ad2antrl 764 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → {𝑑} ⊆ 𝐴) |
36 | 33, 35 | unssd 3789 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → (𝑏 ∪ {𝑑}) ⊆ 𝐴) |
37 | | vex 3203 |
. . . . . . . . . . . . . . 15
⊢ 𝑏 ∈ V |
38 | | snex 4908 |
. . . . . . . . . . . . . . 15
⊢ {𝑑} ∈ V |
39 | 37, 38 | unex 6956 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∪ {𝑑}) ∈ V |
40 | 39 | elpw 4164 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∪ {𝑑}) ∈ 𝒫 𝐴 ↔ (𝑏 ∪ {𝑑}) ⊆ 𝐴) |
41 | 36, 40 | sylibr 224 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → (𝑏 ∪ {𝑑}) ∈ 𝒫 𝐴) |
42 | 29, 41 | elind 3798 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → (𝑏 ∪ {𝑑}) ∈ (Fin ∩ 𝒫 𝐴)) |
43 | | disjsn 4246 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ∩ {𝑑}) = ∅ ↔ ¬ 𝑑 ∈ 𝑏) |
44 | 43 | biimpri 218 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑑 ∈ 𝑏 → (𝑏 ∩ {𝑑}) = ∅) |
45 | | vex 3203 |
. . . . . . . . . . . . . . 15
⊢ 𝑑 ∈ V |
46 | 45 | snnz 4309 |
. . . . . . . . . . . . . 14
⊢ {𝑑} ≠ ∅ |
47 | | disjpss 4028 |
. . . . . . . . . . . . . 14
⊢ (((𝑏 ∩ {𝑑}) = ∅ ∧ {𝑑} ≠ ∅) → 𝑏 ⊊ (𝑏 ∪ {𝑑})) |
48 | 44, 46, 47 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ (¬
𝑑 ∈ 𝑏 → 𝑏 ⊊ (𝑏 ∪ {𝑑})) |
49 | 48 | ad2antll 765 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → 𝑏 ⊊ (𝑏 ∪ {𝑑})) |
50 | 39, 37 | brcnv 5305 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∪ {𝑑})◡
[⊊] 𝑏 ↔
𝑏 [⊊] (𝑏 ∪ {𝑑})) |
51 | 39 | brrpss 6940 |
. . . . . . . . . . . . 13
⊢ (𝑏 [⊊] (𝑏 ∪ {𝑑}) ↔ 𝑏 ⊊ (𝑏 ∪ {𝑑})) |
52 | 50, 51 | bitri 264 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∪ {𝑑})◡
[⊊] 𝑏 ↔
𝑏 ⊊ (𝑏 ∪ {𝑑})) |
53 | 49, 52 | sylibr 224 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → (𝑏 ∪ {𝑑})◡
[⊊] 𝑏) |
54 | | breq1 4656 |
. . . . . . . . . . . 12
⊢ (𝑐 = (𝑏 ∪ {𝑑}) → (𝑐◡
[⊊] 𝑏 ↔
(𝑏 ∪ {𝑑})◡ [⊊] 𝑏)) |
55 | 54 | rspcev 3309 |
. . . . . . . . . . 11
⊢ (((𝑏 ∪ {𝑑}) ∈ (Fin ∩ 𝒫 𝐴) ∧ (𝑏 ∪ {𝑑})◡
[⊊] 𝑏) →
∃𝑐 ∈ (Fin ∩
𝒫 𝐴)𝑐◡ [⊊] 𝑏) |
56 | 42, 53, 55 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → ∃𝑐 ∈ (Fin ∩ 𝒫 𝐴)𝑐◡
[⊊] 𝑏) |
57 | 56 | expr 643 |
. . . . . . . . 9
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ 𝑑 ∈ 𝐴) → (¬ 𝑑 ∈ 𝑏 → ∃𝑐 ∈ (Fin ∩ 𝒫 𝐴)𝑐◡
[⊊] 𝑏)) |
58 | 57 | con1d 139 |
. . . . . . . 8
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ 𝑑 ∈ 𝐴) → (¬ ∃𝑐 ∈ (Fin ∩ 𝒫 𝐴)𝑐◡
[⊊] 𝑏 →
𝑑 ∈ 𝑏)) |
59 | 24, 58 | syl5bi 232 |
. . . . . . 7
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ 𝑑 ∈ 𝐴) → (∀𝑐 ∈ (Fin ∩ 𝒫 𝐴) ¬ 𝑐◡
[⊊] 𝑏 →
𝑑 ∈ 𝑏)) |
60 | 59 | impancom 456 |
. . . . . 6
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ ∀𝑐 ∈ (Fin ∩ 𝒫
𝐴) ¬ 𝑐◡
[⊊] 𝑏) →
(𝑑 ∈ 𝐴 → 𝑑 ∈ 𝑏)) |
61 | 60 | ssrdv 3609 |
. . . . 5
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ ∀𝑐 ∈ (Fin ∩ 𝒫
𝐴) ¬ 𝑐◡
[⊊] 𝑏) →
𝐴 ⊆ 𝑏) |
62 | | ssfi 8180 |
. . . . 5
⊢ ((𝑏 ∈ Fin ∧ 𝐴 ⊆ 𝑏) → 𝐴 ∈ Fin) |
63 | 23, 61, 62 | syl2anc 693 |
. . . 4
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ ∀𝑐 ∈ (Fin ∩ 𝒫
𝐴) ¬ 𝑐◡
[⊊] 𝑏) →
𝐴 ∈
Fin) |
64 | 63 | rexlimiva 3028 |
. . 3
⊢
(∃𝑏 ∈
(Fin ∩ 𝒫 𝐴)∀𝑐 ∈ (Fin ∩ 𝒫 𝐴) ¬ 𝑐◡
[⊊] 𝑏 →
𝐴 ∈
Fin) |
65 | 20, 64 | syl6 35 |
. 2
⊢ (𝐴 ∈ 𝑉 → (◡ [⊊] Fr 𝒫 𝐴 → 𝐴 ∈ Fin)) |
66 | 7, 65 | impbid2 216 |
1
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Fin ↔ ◡ [⊊] Fr 𝒫 𝐴)) |