| Step | Hyp | Ref
| Expression |
| 1 | | difexg 5329 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝑥) ∈ V) |
| 2 | 1 | ralrimivw 3150 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ∀𝑥 ∈ 𝒫 𝐴(𝐴 ∖ 𝑥) ∈ V) |
| 3 | | compss.a |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥)) |
| 4 | 3 | fnmpt 6708 |
. . . 4
⊢
(∀𝑥 ∈
𝒫 𝐴(𝐴 ∖ 𝑥) ∈ V → 𝐹 Fn 𝒫 𝐴) |
| 5 | 2, 4 | syl 17 |
. . 3
⊢ (𝐴 ∈ 𝑉 → 𝐹 Fn 𝒫 𝐴) |
| 6 | 3 | compsscnv 10411 |
. . . . 5
⊢ ◡𝐹 = 𝐹 |
| 7 | 6 | fneq1i 6665 |
. . . 4
⊢ (◡𝐹 Fn 𝒫 𝐴 ↔ 𝐹 Fn 𝒫 𝐴) |
| 8 | 5, 7 | sylibr 234 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ◡𝐹 Fn 𝒫 𝐴) |
| 9 | | dff1o4 6856 |
. . 3
⊢ (𝐹:𝒫 𝐴–1-1-onto→𝒫 𝐴 ↔ (𝐹 Fn 𝒫 𝐴 ∧ ◡𝐹 Fn 𝒫 𝐴)) |
| 10 | 5, 8, 9 | sylanbrc 583 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐹:𝒫 𝐴–1-1-onto→𝒫 𝐴) |
| 11 | | elpwi 4607 |
. . . . . . . . 9
⊢ (𝑏 ∈ 𝒫 𝐴 → 𝑏 ⊆ 𝐴) |
| 12 | 11 | ad2antll 729 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → 𝑏 ⊆ 𝐴) |
| 13 | 3 | isf34lem1 10412 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝐴) → (𝐹‘𝑏) = (𝐴 ∖ 𝑏)) |
| 14 | 12, 13 | syldan 591 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝐹‘𝑏) = (𝐴 ∖ 𝑏)) |
| 15 | | elpwi 4607 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝒫 𝐴 → 𝑎 ⊆ 𝐴) |
| 16 | 15 | ad2antrl 728 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → 𝑎 ⊆ 𝐴) |
| 17 | 3 | isf34lem1 10412 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑎 ⊆ 𝐴) → (𝐹‘𝑎) = (𝐴 ∖ 𝑎)) |
| 18 | 16, 17 | syldan 591 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝐹‘𝑎) = (𝐴 ∖ 𝑎)) |
| 19 | 14, 18 | psseq12d 4097 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → ((𝐹‘𝑏) ⊊ (𝐹‘𝑎) ↔ (𝐴 ∖ 𝑏) ⊊ (𝐴 ∖ 𝑎))) |
| 20 | | difss 4136 |
. . . . . . 7
⊢ (𝐴 ∖ 𝑎) ⊆ 𝐴 |
| 21 | | pssdifcom1 4490 |
. . . . . . 7
⊢ ((𝑏 ⊆ 𝐴 ∧ (𝐴 ∖ 𝑎) ⊆ 𝐴) → ((𝐴 ∖ 𝑏) ⊊ (𝐴 ∖ 𝑎) ↔ (𝐴 ∖ (𝐴 ∖ 𝑎)) ⊊ 𝑏)) |
| 22 | 12, 20, 21 | sylancl 586 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → ((𝐴 ∖ 𝑏) ⊊ (𝐴 ∖ 𝑎) ↔ (𝐴 ∖ (𝐴 ∖ 𝑎)) ⊊ 𝑏)) |
| 23 | | dfss4 4269 |
. . . . . . . 8
⊢ (𝑎 ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ 𝑎)) = 𝑎) |
| 24 | 16, 23 | sylib 218 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝐴 ∖ (𝐴 ∖ 𝑎)) = 𝑎) |
| 25 | 24 | psseq1d 4095 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → ((𝐴 ∖ (𝐴 ∖ 𝑎)) ⊊ 𝑏 ↔ 𝑎 ⊊ 𝑏)) |
| 26 | 19, 22, 25 | 3bitrrd 306 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝑎 ⊊ 𝑏 ↔ (𝐹‘𝑏) ⊊ (𝐹‘𝑎))) |
| 27 | | vex 3484 |
. . . . . 6
⊢ 𝑏 ∈ V |
| 28 | 27 | brrpss 7746 |
. . . . 5
⊢ (𝑎 [⊊] 𝑏 ↔ 𝑎 ⊊ 𝑏) |
| 29 | | fvex 6919 |
. . . . . 6
⊢ (𝐹‘𝑎) ∈ V |
| 30 | 29 | brrpss 7746 |
. . . . 5
⊢ ((𝐹‘𝑏) [⊊] (𝐹‘𝑎) ↔ (𝐹‘𝑏) ⊊ (𝐹‘𝑎)) |
| 31 | 26, 28, 30 | 3bitr4g 314 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝑎 [⊊] 𝑏 ↔ (𝐹‘𝑏) [⊊] (𝐹‘𝑎))) |
| 32 | | relrpss 7744 |
. . . . 5
⊢ Rel
[⊊] |
| 33 | 32 | relbrcnv 6125 |
. . . 4
⊢ ((𝐹‘𝑎)◡
[⊊] (𝐹‘𝑏) ↔ (𝐹‘𝑏) [⊊] (𝐹‘𝑎)) |
| 34 | 31, 33 | bitr4di 289 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝑎 [⊊] 𝑏 ↔ (𝐹‘𝑎)◡
[⊊] (𝐹‘𝑏))) |
| 35 | 34 | ralrimivva 3202 |
. 2
⊢ (𝐴 ∈ 𝑉 → ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴(𝑎 [⊊] 𝑏 ↔ (𝐹‘𝑎)◡
[⊊] (𝐹‘𝑏))) |
| 36 | | df-isom 6570 |
. 2
⊢ (𝐹 Isom [⊊] , ◡ [⊊] (𝒫 𝐴, 𝒫 𝐴) ↔ (𝐹:𝒫 𝐴–1-1-onto→𝒫 𝐴 ∧ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴(𝑎 [⊊] 𝑏 ↔ (𝐹‘𝑎)◡
[⊊] (𝐹‘𝑏)))) |
| 37 | 10, 35, 36 | sylanbrc 583 |
1
⊢ (𝐴 ∈ 𝑉 → 𝐹 Isom [⊊] , ◡ [⊊] (𝒫 𝐴, 𝒫 𝐴)) |