Proof of Theorem isf34lem5
Step | Hyp | Ref
| Expression |
1 | | imassrn 5396 |
. . . . . . 7
⊢ (𝐹 “ 𝑋) ⊆ ran 𝐹 |
2 | | compss.a |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥)) |
3 | 2 | isf34lem2 9078 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → 𝐹:𝒫 𝐴⟶𝒫 𝐴) |
4 | 3 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → 𝐹:𝒫 𝐴⟶𝒫 𝐴) |
5 | | frn 5966 |
. . . . . . . 8
⊢ (𝐹:𝒫 𝐴⟶𝒫 𝐴 → ran 𝐹 ⊆ 𝒫 𝐴) |
6 | 4, 5 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → ran 𝐹 ⊆ 𝒫 𝐴) |
7 | 1, 6 | syl5ss 3579 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐹 “ 𝑋) ⊆ 𝒫 𝐴) |
8 | | simprl 790 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → 𝑋 ⊆ 𝒫 𝐴) |
9 | | fdm 5964 |
. . . . . . . . . . 11
⊢ (𝐹:𝒫 𝐴⟶𝒫 𝐴 → dom 𝐹 = 𝒫 𝐴) |
10 | 4, 9 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → dom 𝐹 = 𝒫 𝐴) |
11 | 8, 10 | sseqtr4d 3605 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → 𝑋 ⊆ dom 𝐹) |
12 | | sseqin2 3779 |
. . . . . . . . 9
⊢ (𝑋 ⊆ dom 𝐹 ↔ (dom 𝐹 ∩ 𝑋) = 𝑋) |
13 | 11, 12 | sylib 207 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (dom 𝐹 ∩ 𝑋) = 𝑋) |
14 | | simprr 792 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → 𝑋 ≠ ∅) |
15 | 13, 14 | eqnetrd 2849 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (dom 𝐹 ∩ 𝑋) ≠ ∅) |
16 | | imadisj 5403 |
. . . . . . . 8
⊢ ((𝐹 “ 𝑋) = ∅ ↔ (dom 𝐹 ∩ 𝑋) = ∅) |
17 | 16 | necon3bii 2834 |
. . . . . . 7
⊢ ((𝐹 “ 𝑋) ≠ ∅ ↔ (dom 𝐹 ∩ 𝑋) ≠ ∅) |
18 | 15, 17 | sylibr 223 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐹 “ 𝑋) ≠ ∅) |
19 | 7, 18 | jca 553 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → ((𝐹 “ 𝑋) ⊆ 𝒫 𝐴 ∧ (𝐹 “ 𝑋) ≠ ∅)) |
20 | 2 | isf34lem4 9082 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ ((𝐹 “ 𝑋) ⊆ 𝒫 𝐴 ∧ (𝐹 “ 𝑋) ≠ ∅)) → (𝐹‘∪ (𝐹 “ 𝑋)) = ∩ (𝐹 “ (𝐹 “ 𝑋))) |
21 | 19, 20 | syldan 486 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐹‘∪ (𝐹 “ 𝑋)) = ∩ (𝐹 “ (𝐹 “ 𝑋))) |
22 | 2 | isf34lem3 9080 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) → (𝐹 “ (𝐹 “ 𝑋)) = 𝑋) |
23 | 22 | adantrr 749 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐹 “ (𝐹 “ 𝑋)) = 𝑋) |
24 | 23 | inteqd 4415 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → ∩ (𝐹
“ (𝐹 “ 𝑋)) = ∩ 𝑋) |
25 | 21, 24 | eqtrd 2644 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐹‘∪ (𝐹 “ 𝑋)) = ∩ 𝑋) |
26 | 25 | fveq2d 6107 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐹‘(𝐹‘∪ (𝐹 “ 𝑋))) = (𝐹‘∩ 𝑋)) |
27 | 2 | compsscnv 9076 |
. . . 4
⊢ ◡𝐹 = 𝐹 |
28 | 27 | fveq1i 6104 |
. . 3
⊢ (◡𝐹‘(𝐹‘∪ (𝐹 “ 𝑋))) = (𝐹‘(𝐹‘∪ (𝐹 “ 𝑋))) |
29 | 2 | compssiso 9079 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝐹 Isom [⊊] , ◡ [⊊] (𝒫 𝐴, 𝒫 𝐴)) |
30 | | isof1o 6473 |
. . . . . 6
⊢ (𝐹 Isom [⊊] , ◡ [⊊] (𝒫 𝐴, 𝒫 𝐴) → 𝐹:𝒫 𝐴–1-1-onto→𝒫 𝐴) |
31 | 29, 30 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → 𝐹:𝒫 𝐴–1-1-onto→𝒫 𝐴) |
32 | 31 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → 𝐹:𝒫 𝐴–1-1-onto→𝒫 𝐴) |
33 | | sspwuni 4547 |
. . . . . 6
⊢ ((𝐹 “ 𝑋) ⊆ 𝒫 𝐴 ↔ ∪ (𝐹 “ 𝑋) ⊆ 𝐴) |
34 | 7, 33 | sylib 207 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → ∪ (𝐹
“ 𝑋) ⊆ 𝐴) |
35 | | elpw2g 4754 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (∪ (𝐹 “ 𝑋) ∈ 𝒫 𝐴 ↔ ∪ (𝐹 “ 𝑋) ⊆ 𝐴)) |
36 | 35 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (∪ (𝐹
“ 𝑋) ∈ 𝒫
𝐴 ↔ ∪ (𝐹
“ 𝑋) ⊆ 𝐴)) |
37 | 34, 36 | mpbird 246 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → ∪ (𝐹
“ 𝑋) ∈ 𝒫
𝐴) |
38 | | f1ocnvfv1 6432 |
. . . 4
⊢ ((𝐹:𝒫 𝐴–1-1-onto→𝒫 𝐴 ∧ ∪ (𝐹 “ 𝑋) ∈ 𝒫 𝐴) → (◡𝐹‘(𝐹‘∪ (𝐹 “ 𝑋))) = ∪ (𝐹 “ 𝑋)) |
39 | 32, 37, 38 | syl2anc 691 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (◡𝐹‘(𝐹‘∪ (𝐹 “ 𝑋))) = ∪ (𝐹 “ 𝑋)) |
40 | 28, 39 | syl5eqr 2658 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐹‘(𝐹‘∪ (𝐹 “ 𝑋))) = ∪ (𝐹 “ 𝑋)) |
41 | 26, 40 | eqtr3d 2646 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐹‘∩ 𝑋) = ∪
(𝐹 “ 𝑋)) |