Step | Hyp | Ref
| Expression |
1 | | porpss 7669 |
. . . 4
⊢
[⊊] Po 𝒫 𝐴 |
2 | | cnvpo 6244 |
. . . 4
⊢ (
[⊊] Po 𝒫 𝐴 ↔ ◡ [⊊] Po 𝒫 𝐴) |
3 | 1, 2 | mpbi 229 |
. . 3
⊢ ◡ [⊊] Po 𝒫 𝐴 |
4 | | pwfi 9129 |
. . . 4
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Fin) |
5 | 4 | biimpi 215 |
. . 3
⊢ (𝐴 ∈ Fin → 𝒫
𝐴 ∈
Fin) |
6 | | frfi 9239 |
. . 3
⊢ ((◡ [⊊] Po 𝒫 𝐴 ∧ 𝒫 𝐴 ∈ Fin) → ◡ [⊊] Fr 𝒫 𝐴) |
7 | 3, 5, 6 | sylancr 588 |
. 2
⊢ (𝐴 ∈ Fin → ◡ [⊊] Fr 𝒫 𝐴) |
8 | | inss2 4194 |
. . . . . 6
⊢ (Fin
∩ 𝒫 𝐴) ⊆
𝒫 𝐴 |
9 | | pwexg 5338 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
10 | | ssexg 5285 |
. . . . . 6
⊢ (((Fin
∩ 𝒫 𝐴) ⊆
𝒫 𝐴 ∧ 𝒫
𝐴 ∈ V) → (Fin
∩ 𝒫 𝐴) ∈
V) |
11 | 8, 9, 10 | sylancr 588 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (Fin ∩ 𝒫 𝐴) ∈ V) |
12 | | 0fin 9122 |
. . . . . . . 8
⊢ ∅
∈ Fin |
13 | | 0elpw 5316 |
. . . . . . . 8
⊢ ∅
∈ 𝒫 𝐴 |
14 | 12, 13 | elini 4158 |
. . . . . . 7
⊢ ∅
∈ (Fin ∩ 𝒫 𝐴) |
15 | 14 | ne0ii 4302 |
. . . . . 6
⊢ (Fin
∩ 𝒫 𝐴) ≠
∅ |
16 | | fri 5598 |
. . . . . 6
⊢ ((((Fin
∩ 𝒫 𝐴) ∈ V
∧ ◡ [⊊] Fr 𝒫
𝐴) ∧ ((Fin ∩
𝒫 𝐴) ⊆
𝒫 𝐴 ∧ (Fin
∩ 𝒫 𝐴) ≠
∅)) → ∃𝑏
∈ (Fin ∩ 𝒫 𝐴)∀𝑐 ∈ (Fin ∩ 𝒫 𝐴) ¬ 𝑐◡
[⊊] 𝑏) |
17 | 8, 15, 16 | mpanr12 704 |
. . . . 5
⊢ (((Fin
∩ 𝒫 𝐴) ∈ V
∧ ◡ [⊊] Fr 𝒫
𝐴) → ∃𝑏 ∈ (Fin ∩ 𝒫
𝐴)∀𝑐 ∈ (Fin ∩ 𝒫
𝐴) ¬ 𝑐◡
[⊊] 𝑏) |
18 | 11, 17 | sylan 581 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ◡ [⊊] Fr 𝒫 𝐴) → ∃𝑏 ∈ (Fin ∩ 𝒫
𝐴)∀𝑐 ∈ (Fin ∩ 𝒫
𝐴) ¬ 𝑐◡
[⊊] 𝑏) |
19 | 18 | ex 414 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (◡ [⊊] Fr 𝒫 𝐴 → ∃𝑏 ∈ (Fin ∩ 𝒫
𝐴)∀𝑐 ∈ (Fin ∩ 𝒫
𝐴) ¬ 𝑐◡
[⊊] 𝑏)) |
20 | | elinel1 4160 |
. . . . 5
⊢ (𝑏 ∈ (Fin ∩ 𝒫
𝐴) → 𝑏 ∈ Fin) |
21 | | ralnex 3076 |
. . . . . . . 8
⊢
(∀𝑐 ∈
(Fin ∩ 𝒫 𝐴)
¬ 𝑐◡ [⊊] 𝑏 ↔ ¬ ∃𝑐 ∈ (Fin ∩ 𝒫 𝐴)𝑐◡
[⊊] 𝑏) |
22 | 20 | adantr 482 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → 𝑏 ∈ Fin) |
23 | | snfi 8995 |
. . . . . . . . . . . . 13
⊢ {𝑑} ∈ Fin |
24 | | unfi 9123 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ Fin ∧ {𝑑} ∈ Fin) → (𝑏 ∪ {𝑑}) ∈ Fin) |
25 | 22, 23, 24 | sylancl 587 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → (𝑏 ∪ {𝑑}) ∈ Fin) |
26 | | elinel2 4161 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ (Fin ∩ 𝒫
𝐴) → 𝑏 ∈ 𝒫 𝐴) |
27 | 26 | elpwid 4574 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ (Fin ∩ 𝒫
𝐴) → 𝑏 ⊆ 𝐴) |
28 | 27 | adantr 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → 𝑏 ⊆ 𝐴) |
29 | | snssi 4773 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 ∈ 𝐴 → {𝑑} ⊆ 𝐴) |
30 | 29 | ad2antrl 727 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → {𝑑} ⊆ 𝐴) |
31 | 28, 30 | unssd 4151 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → (𝑏 ∪ {𝑑}) ⊆ 𝐴) |
32 | | vex 3452 |
. . . . . . . . . . . . . . 15
⊢ 𝑏 ∈ V |
33 | | vsnex 5391 |
. . . . . . . . . . . . . . 15
⊢ {𝑑} ∈ V |
34 | 32, 33 | unex 7685 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∪ {𝑑}) ∈ V |
35 | 34 | elpw 4569 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∪ {𝑑}) ∈ 𝒫 𝐴 ↔ (𝑏 ∪ {𝑑}) ⊆ 𝐴) |
36 | 31, 35 | sylibr 233 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → (𝑏 ∪ {𝑑}) ∈ 𝒫 𝐴) |
37 | 25, 36 | elind 4159 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → (𝑏 ∪ {𝑑}) ∈ (Fin ∩ 𝒫 𝐴)) |
38 | | disjsn 4677 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ∩ {𝑑}) = ∅ ↔ ¬ 𝑑 ∈ 𝑏) |
39 | 38 | biimpri 227 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑑 ∈ 𝑏 → (𝑏 ∩ {𝑑}) = ∅) |
40 | | vex 3452 |
. . . . . . . . . . . . . . 15
⊢ 𝑑 ∈ V |
41 | 40 | snnz 4742 |
. . . . . . . . . . . . . 14
⊢ {𝑑} ≠ ∅ |
42 | | disjpss 4425 |
. . . . . . . . . . . . . 14
⊢ (((𝑏 ∩ {𝑑}) = ∅ ∧ {𝑑} ≠ ∅) → 𝑏 ⊊ (𝑏 ∪ {𝑑})) |
43 | 39, 41, 42 | sylancl 587 |
. . . . . . . . . . . . 13
⊢ (¬
𝑑 ∈ 𝑏 → 𝑏 ⊊ (𝑏 ∪ {𝑑})) |
44 | 43 | ad2antll 728 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → 𝑏 ⊊ (𝑏 ∪ {𝑑})) |
45 | 34, 32 | brcnv 5843 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∪ {𝑑})◡
[⊊] 𝑏 ↔
𝑏 [⊊] (𝑏 ∪ {𝑑})) |
46 | 34 | brrpss 7668 |
. . . . . . . . . . . . 13
⊢ (𝑏 [⊊] (𝑏 ∪ {𝑑}) ↔ 𝑏 ⊊ (𝑏 ∪ {𝑑})) |
47 | 45, 46 | bitri 275 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∪ {𝑑})◡
[⊊] 𝑏 ↔
𝑏 ⊊ (𝑏 ∪ {𝑑})) |
48 | 44, 47 | sylibr 233 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → (𝑏 ∪ {𝑑})◡
[⊊] 𝑏) |
49 | | breq1 5113 |
. . . . . . . . . . . 12
⊢ (𝑐 = (𝑏 ∪ {𝑑}) → (𝑐◡
[⊊] 𝑏 ↔
(𝑏 ∪ {𝑑})◡ [⊊] 𝑏)) |
50 | 49 | rspcev 3584 |
. . . . . . . . . . 11
⊢ (((𝑏 ∪ {𝑑}) ∈ (Fin ∩ 𝒫 𝐴) ∧ (𝑏 ∪ {𝑑})◡
[⊊] 𝑏) →
∃𝑐 ∈ (Fin ∩
𝒫 𝐴)𝑐◡ [⊊] 𝑏) |
51 | 37, 48, 50 | syl2anc 585 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → ∃𝑐 ∈ (Fin ∩ 𝒫 𝐴)𝑐◡
[⊊] 𝑏) |
52 | 51 | expr 458 |
. . . . . . . . 9
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ 𝑑 ∈ 𝐴) → (¬ 𝑑 ∈ 𝑏 → ∃𝑐 ∈ (Fin ∩ 𝒫 𝐴)𝑐◡
[⊊] 𝑏)) |
53 | 52 | con1d 145 |
. . . . . . . 8
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ 𝑑 ∈ 𝐴) → (¬ ∃𝑐 ∈ (Fin ∩ 𝒫 𝐴)𝑐◡
[⊊] 𝑏 →
𝑑 ∈ 𝑏)) |
54 | 21, 53 | biimtrid 241 |
. . . . . . 7
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ 𝑑 ∈ 𝐴) → (∀𝑐 ∈ (Fin ∩ 𝒫 𝐴) ¬ 𝑐◡
[⊊] 𝑏 →
𝑑 ∈ 𝑏)) |
55 | 54 | impancom 453 |
. . . . . 6
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ ∀𝑐 ∈ (Fin ∩ 𝒫
𝐴) ¬ 𝑐◡
[⊊] 𝑏) →
(𝑑 ∈ 𝐴 → 𝑑 ∈ 𝑏)) |
56 | 55 | ssrdv 3955 |
. . . . 5
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ ∀𝑐 ∈ (Fin ∩ 𝒫
𝐴) ¬ 𝑐◡
[⊊] 𝑏) →
𝐴 ⊆ 𝑏) |
57 | | ssfi 9124 |
. . . . 5
⊢ ((𝑏 ∈ Fin ∧ 𝐴 ⊆ 𝑏) → 𝐴 ∈ Fin) |
58 | 20, 56, 57 | syl2an2r 684 |
. . . 4
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ ∀𝑐 ∈ (Fin ∩ 𝒫
𝐴) ¬ 𝑐◡
[⊊] 𝑏) →
𝐴 ∈
Fin) |
59 | 58 | rexlimiva 3145 |
. . 3
⊢
(∃𝑏 ∈
(Fin ∩ 𝒫 𝐴)∀𝑐 ∈ (Fin ∩ 𝒫 𝐴) ¬ 𝑐◡
[⊊] 𝑏 →
𝐴 ∈
Fin) |
60 | 19, 59 | syl6 35 |
. 2
⊢ (𝐴 ∈ 𝑉 → (◡ [⊊] Fr 𝒫 𝐴 → 𝐴 ∈ Fin)) |
61 | 7, 60 | impbid2 225 |
1
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Fin ↔ ◡ [⊊] Fr 𝒫 𝐴)) |