| Step | Hyp | Ref
| Expression |
| 1 | | porpss 7747 |
. . . 4
⊢
[⊊] Po 𝒫 𝐴 |
| 2 | | cnvpo 6307 |
. . . 4
⊢ (
[⊊] Po 𝒫 𝐴 ↔ ◡ [⊊] Po 𝒫 𝐴) |
| 3 | 1, 2 | mpbi 230 |
. . 3
⊢ ◡ [⊊] Po 𝒫 𝐴 |
| 4 | | pwfi 9357 |
. . . 4
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Fin) |
| 5 | 4 | biimpi 216 |
. . 3
⊢ (𝐴 ∈ Fin → 𝒫
𝐴 ∈
Fin) |
| 6 | | frfi 9321 |
. . 3
⊢ ((◡ [⊊] Po 𝒫 𝐴 ∧ 𝒫 𝐴 ∈ Fin) → ◡ [⊊] Fr 𝒫 𝐴) |
| 7 | 3, 5, 6 | sylancr 587 |
. 2
⊢ (𝐴 ∈ Fin → ◡ [⊊] Fr 𝒫 𝐴) |
| 8 | | inss2 4238 |
. . . . . 6
⊢ (Fin
∩ 𝒫 𝐴) ⊆
𝒫 𝐴 |
| 9 | | pwexg 5378 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
| 10 | | ssexg 5323 |
. . . . . 6
⊢ (((Fin
∩ 𝒫 𝐴) ⊆
𝒫 𝐴 ∧ 𝒫
𝐴 ∈ V) → (Fin
∩ 𝒫 𝐴) ∈
V) |
| 11 | 8, 9, 10 | sylancr 587 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (Fin ∩ 𝒫 𝐴) ∈ V) |
| 12 | | 0fi 9082 |
. . . . . . . 8
⊢ ∅
∈ Fin |
| 13 | | 0elpw 5356 |
. . . . . . . 8
⊢ ∅
∈ 𝒫 𝐴 |
| 14 | 12, 13 | elini 4199 |
. . . . . . 7
⊢ ∅
∈ (Fin ∩ 𝒫 𝐴) |
| 15 | 14 | ne0ii 4344 |
. . . . . 6
⊢ (Fin
∩ 𝒫 𝐴) ≠
∅ |
| 16 | | fri 5642 |
. . . . . 6
⊢ ((((Fin
∩ 𝒫 𝐴) ∈ V
∧ ◡ [⊊] Fr 𝒫
𝐴) ∧ ((Fin ∩
𝒫 𝐴) ⊆
𝒫 𝐴 ∧ (Fin
∩ 𝒫 𝐴) ≠
∅)) → ∃𝑏
∈ (Fin ∩ 𝒫 𝐴)∀𝑐 ∈ (Fin ∩ 𝒫 𝐴) ¬ 𝑐◡
[⊊] 𝑏) |
| 17 | 8, 15, 16 | mpanr12 705 |
. . . . 5
⊢ (((Fin
∩ 𝒫 𝐴) ∈ V
∧ ◡ [⊊] Fr 𝒫
𝐴) → ∃𝑏 ∈ (Fin ∩ 𝒫
𝐴)∀𝑐 ∈ (Fin ∩ 𝒫
𝐴) ¬ 𝑐◡
[⊊] 𝑏) |
| 18 | 11, 17 | sylan 580 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ◡ [⊊] Fr 𝒫 𝐴) → ∃𝑏 ∈ (Fin ∩ 𝒫
𝐴)∀𝑐 ∈ (Fin ∩ 𝒫
𝐴) ¬ 𝑐◡
[⊊] 𝑏) |
| 19 | 18 | ex 412 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (◡ [⊊] Fr 𝒫 𝐴 → ∃𝑏 ∈ (Fin ∩ 𝒫
𝐴)∀𝑐 ∈ (Fin ∩ 𝒫
𝐴) ¬ 𝑐◡
[⊊] 𝑏)) |
| 20 | | elinel1 4201 |
. . . . 5
⊢ (𝑏 ∈ (Fin ∩ 𝒫
𝐴) → 𝑏 ∈ Fin) |
| 21 | | ralnex 3072 |
. . . . . . . 8
⊢
(∀𝑐 ∈
(Fin ∩ 𝒫 𝐴)
¬ 𝑐◡ [⊊] 𝑏 ↔ ¬ ∃𝑐 ∈ (Fin ∩ 𝒫 𝐴)𝑐◡
[⊊] 𝑏) |
| 22 | 20 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → 𝑏 ∈ Fin) |
| 23 | | snfi 9083 |
. . . . . . . . . . . . 13
⊢ {𝑑} ∈ Fin |
| 24 | | unfi 9211 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ Fin ∧ {𝑑} ∈ Fin) → (𝑏 ∪ {𝑑}) ∈ Fin) |
| 25 | 22, 23, 24 | sylancl 586 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → (𝑏 ∪ {𝑑}) ∈ Fin) |
| 26 | | elinel2 4202 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ (Fin ∩ 𝒫
𝐴) → 𝑏 ∈ 𝒫 𝐴) |
| 27 | 26 | elpwid 4609 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ (Fin ∩ 𝒫
𝐴) → 𝑏 ⊆ 𝐴) |
| 28 | 27 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → 𝑏 ⊆ 𝐴) |
| 29 | | snssi 4808 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 ∈ 𝐴 → {𝑑} ⊆ 𝐴) |
| 30 | 29 | ad2antrl 728 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → {𝑑} ⊆ 𝐴) |
| 31 | 28, 30 | unssd 4192 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → (𝑏 ∪ {𝑑}) ⊆ 𝐴) |
| 32 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑏 ∈ V |
| 33 | | vsnex 5434 |
. . . . . . . . . . . . . . 15
⊢ {𝑑} ∈ V |
| 34 | 32, 33 | unex 7764 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∪ {𝑑}) ∈ V |
| 35 | 34 | elpw 4604 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∪ {𝑑}) ∈ 𝒫 𝐴 ↔ (𝑏 ∪ {𝑑}) ⊆ 𝐴) |
| 36 | 31, 35 | sylibr 234 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → (𝑏 ∪ {𝑑}) ∈ 𝒫 𝐴) |
| 37 | 25, 36 | elind 4200 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → (𝑏 ∪ {𝑑}) ∈ (Fin ∩ 𝒫 𝐴)) |
| 38 | | disjsn 4711 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ∩ {𝑑}) = ∅ ↔ ¬ 𝑑 ∈ 𝑏) |
| 39 | 38 | biimpri 228 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑑 ∈ 𝑏 → (𝑏 ∩ {𝑑}) = ∅) |
| 40 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑑 ∈ V |
| 41 | 40 | snnz 4776 |
. . . . . . . . . . . . . 14
⊢ {𝑑} ≠ ∅ |
| 42 | | disjpss 4461 |
. . . . . . . . . . . . . 14
⊢ (((𝑏 ∩ {𝑑}) = ∅ ∧ {𝑑} ≠ ∅) → 𝑏 ⊊ (𝑏 ∪ {𝑑})) |
| 43 | 39, 41, 42 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ (¬
𝑑 ∈ 𝑏 → 𝑏 ⊊ (𝑏 ∪ {𝑑})) |
| 44 | 43 | ad2antll 729 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → 𝑏 ⊊ (𝑏 ∪ {𝑑})) |
| 45 | 34, 32 | brcnv 5893 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∪ {𝑑})◡
[⊊] 𝑏 ↔
𝑏 [⊊] (𝑏 ∪ {𝑑})) |
| 46 | 34 | brrpss 7746 |
. . . . . . . . . . . . 13
⊢ (𝑏 [⊊] (𝑏 ∪ {𝑑}) ↔ 𝑏 ⊊ (𝑏 ∪ {𝑑})) |
| 47 | 45, 46 | bitri 275 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∪ {𝑑})◡
[⊊] 𝑏 ↔
𝑏 ⊊ (𝑏 ∪ {𝑑})) |
| 48 | 44, 47 | sylibr 234 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → (𝑏 ∪ {𝑑})◡
[⊊] 𝑏) |
| 49 | | breq1 5146 |
. . . . . . . . . . . 12
⊢ (𝑐 = (𝑏 ∪ {𝑑}) → (𝑐◡
[⊊] 𝑏 ↔
(𝑏 ∪ {𝑑})◡ [⊊] 𝑏)) |
| 50 | 49 | rspcev 3622 |
. . . . . . . . . . 11
⊢ (((𝑏 ∪ {𝑑}) ∈ (Fin ∩ 𝒫 𝐴) ∧ (𝑏 ∪ {𝑑})◡
[⊊] 𝑏) →
∃𝑐 ∈ (Fin ∩
𝒫 𝐴)𝑐◡ [⊊] 𝑏) |
| 51 | 37, 48, 50 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ (𝑑 ∈ 𝐴 ∧ ¬ 𝑑 ∈ 𝑏)) → ∃𝑐 ∈ (Fin ∩ 𝒫 𝐴)𝑐◡
[⊊] 𝑏) |
| 52 | 51 | expr 456 |
. . . . . . . . 9
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ 𝑑 ∈ 𝐴) → (¬ 𝑑 ∈ 𝑏 → ∃𝑐 ∈ (Fin ∩ 𝒫 𝐴)𝑐◡
[⊊] 𝑏)) |
| 53 | 52 | con1d 145 |
. . . . . . . 8
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ 𝑑 ∈ 𝐴) → (¬ ∃𝑐 ∈ (Fin ∩ 𝒫 𝐴)𝑐◡
[⊊] 𝑏 →
𝑑 ∈ 𝑏)) |
| 54 | 21, 53 | biimtrid 242 |
. . . . . . 7
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ 𝑑 ∈ 𝐴) → (∀𝑐 ∈ (Fin ∩ 𝒫 𝐴) ¬ 𝑐◡
[⊊] 𝑏 →
𝑑 ∈ 𝑏)) |
| 55 | 54 | impancom 451 |
. . . . . 6
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ ∀𝑐 ∈ (Fin ∩ 𝒫
𝐴) ¬ 𝑐◡
[⊊] 𝑏) →
(𝑑 ∈ 𝐴 → 𝑑 ∈ 𝑏)) |
| 56 | 55 | ssrdv 3989 |
. . . . 5
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ ∀𝑐 ∈ (Fin ∩ 𝒫
𝐴) ¬ 𝑐◡
[⊊] 𝑏) →
𝐴 ⊆ 𝑏) |
| 57 | | ssfi 9213 |
. . . . 5
⊢ ((𝑏 ∈ Fin ∧ 𝐴 ⊆ 𝑏) → 𝐴 ∈ Fin) |
| 58 | 20, 56, 57 | syl2an2r 685 |
. . . 4
⊢ ((𝑏 ∈ (Fin ∩ 𝒫
𝐴) ∧ ∀𝑐 ∈ (Fin ∩ 𝒫
𝐴) ¬ 𝑐◡
[⊊] 𝑏) →
𝐴 ∈
Fin) |
| 59 | 58 | rexlimiva 3147 |
. . 3
⊢
(∃𝑏 ∈
(Fin ∩ 𝒫 𝐴)∀𝑐 ∈ (Fin ∩ 𝒫 𝐴) ¬ 𝑐◡
[⊊] 𝑏 →
𝐴 ∈
Fin) |
| 60 | 19, 59 | syl6 35 |
. 2
⊢ (𝐴 ∈ 𝑉 → (◡ [⊊] Fr 𝒫 𝐴 → 𝐴 ∈ Fin)) |
| 61 | 7, 60 | impbid2 226 |
1
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Fin ↔ ◡ [⊊] Fr 𝒫 𝐴)) |