Step | Hyp | Ref
| Expression |
1 | | brex 4689 |
. 2
⊢ (A ≈ B
→ (A ∈ V ∧ B ∈
V)) |
2 | | breq1 4642 |
. . . 4
⊢ (a = A →
(a ≈ b ↔ A
≈ b)) |
3 | | oveq2 5531 |
. . . . 5
⊢ (a = A →
(C ↑m a) = (C
↑m A)) |
4 | 3 | breq1d 4649 |
. . . 4
⊢ (a = A →
((C ↑m a) ≈ (C
↑m b) ↔
(C ↑m A) ≈ (C
↑m b))) |
5 | 2, 4 | imbi12d 311 |
. . 3
⊢ (a = A →
((a ≈ b → (C
↑m a) ≈
(C ↑m b)) ↔ (A
≈ b → (C ↑m A) ≈ (C
↑m b)))) |
6 | | breq2 4643 |
. . . 4
⊢ (b = B →
(A ≈ b ↔ A
≈ B)) |
7 | | oveq2 5531 |
. . . . 5
⊢ (b = B →
(C ↑m b) = (C
↑m B)) |
8 | 7 | breq2d 4651 |
. . . 4
⊢ (b = B →
((C ↑m A) ≈ (C
↑m b) ↔
(C ↑m A) ≈ (C
↑m B))) |
9 | 6, 8 | imbi12d 311 |
. . 3
⊢ (b = B →
((A ≈ b → (C
↑m A) ≈
(C ↑m b)) ↔ (A
≈ B → (C ↑m A) ≈ (C
↑m B)))) |
10 | | bren 6030 |
. . . 4
⊢ (a ≈ b
↔ ∃r r:a–1-1-onto→b) |
11 | | eqid 2353 |
. . . . . . . . . 10
⊢ (s ∈ (C ↑m a) ↦ (s ∘ ◡r)) =
(s ∈
(C ↑m a) ↦ (s ∘ ◡r)) |
12 | 11 | enmap2lem4 6066 |
. . . . . . . . 9
⊢ (r:a–1-1-onto→b →
Fun ◡(s ∈ (C ↑m a) ↦ (s ∘ ◡r))) |
13 | | dfrn4 4904 |
. . . . . . . . . 10
⊢ ran (s ∈ (C ↑m a) ↦ (s ∘ ◡r)) =
dom ◡(s ∈ (C ↑m a) ↦ (s ∘ ◡r)) |
14 | 11 | enmap2lem5 6067 |
. . . . . . . . . 10
⊢ (r:a–1-1-onto→b →
ran (s ∈
(C ↑m a) ↦ (s ∘ ◡r)) =
(C ↑m b)) |
15 | 13, 14 | syl5eqr 2399 |
. . . . . . . . 9
⊢ (r:a–1-1-onto→b →
dom ◡(s ∈ (C ↑m a) ↦ (s ∘ ◡r)) =
(C ↑m b)) |
16 | 12, 15 | jca 518 |
. . . . . . . 8
⊢ (r:a–1-1-onto→b →
(Fun ◡(s ∈ (C ↑m a) ↦ (s ∘ ◡r))
∧ dom ◡(s ∈ (C
↑m a) ↦ (s ∘ ◡r)) =
(C ↑m b))) |
17 | | df-fn 4790 |
. . . . . . . 8
⊢ (◡(s ∈ (C
↑m a) ↦ (s ∘ ◡r)) Fn
(C ↑m b) ↔ (Fun ◡(s ∈ (C
↑m a) ↦ (s ∘ ◡r))
∧ dom ◡(s ∈ (C
↑m a) ↦ (s ∘ ◡r)) =
(C ↑m b))) |
18 | 16, 17 | sylibr 203 |
. . . . . . 7
⊢ (r:a–1-1-onto→b →
◡(s
∈ (C
↑m a) ↦ (s ∘ ◡r)) Fn
(C ↑m b)) |
19 | 11 | enmap2lem2 6064 |
. . . . . . . 8
⊢ (s ∈ (C ↑m a) ↦ (s ∘ ◡r)) Fn
(C ↑m a) |
20 | | dff1o4 5294 |
. . . . . . . 8
⊢ ((s ∈ (C ↑m a) ↦ (s ∘ ◡r)):(C
↑m a)–1-1-onto→(C
↑m b) ↔
((s ∈
(C ↑m a) ↦ (s ∘ ◡r)) Fn
(C ↑m a) ∧ ◡(s ∈ (C
↑m a) ↦ (s ∘ ◡r)) Fn
(C ↑m b))) |
21 | 19, 20 | mpbiran 884 |
. . . . . . 7
⊢ ((s ∈ (C ↑m a) ↦ (s ∘ ◡r)):(C
↑m a)–1-1-onto→(C
↑m b) ↔ ◡(s ∈ (C
↑m a) ↦ (s ∘ ◡r)) Fn
(C ↑m b)) |
22 | 18, 21 | sylibr 203 |
. . . . . 6
⊢ (r:a–1-1-onto→b →
(s ∈
(C ↑m a) ↦ (s ∘ ◡r)):(C
↑m a)–1-1-onto→(C
↑m b)) |
23 | 11 | enmap2lem1 6063 |
. . . . . . 7
⊢ (s ∈ (C ↑m a) ↦ (s ∘ ◡r))
∈ V |
24 | 23 | f1oen 6033 |
. . . . . 6
⊢ ((s ∈ (C ↑m a) ↦ (s ∘ ◡r)):(C
↑m a)–1-1-onto→(C
↑m b) →
(C ↑m a) ≈ (C
↑m b)) |
25 | 22, 24 | syl 15 |
. . . . 5
⊢ (r:a–1-1-onto→b →
(C ↑m a) ≈ (C
↑m b)) |
26 | 25 | exlimiv 1634 |
. . . 4
⊢ (∃r r:a–1-1-onto→b →
(C ↑m a) ≈ (C
↑m b)) |
27 | 10, 26 | sylbi 187 |
. . 3
⊢ (a ≈ b
→ (C ↑m
a) ≈ (C ↑m b)) |
28 | 5, 9, 27 | vtocl2g 2918 |
. 2
⊢ ((A ∈ V ∧ B ∈ V) → (A
≈ B → (C ↑m A) ≈ (C
↑m B))) |
29 | 1, 28 | mpcom 32 |
1
⊢ (A ≈ B
→ (C ↑m
A) ≈ (C ↑m B)) |