Step | Hyp | Ref
| Expression |
1 | | dfse2 4960 |
. . . . . . . . 9
⊢ (𝑅 Se 𝐴 ↔ ∀𝑧 ∈ 𝐴 (𝐴 ∩ (◡𝑅 “ {𝑧})) ∈ V) |
2 | 1 | biimpi 119 |
. . . . . . . 8
⊢ (𝑅 Se 𝐴 → ∀𝑧 ∈ 𝐴 (𝐴 ∩ (◡𝑅 “ {𝑧})) ∈ V) |
3 | 2 | r19.21bi 2545 |
. . . . . . 7
⊢ ((𝑅 Se 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝐴 ∩ (◡𝑅 “ {𝑧})) ∈ V) |
4 | 3 | expcom 115 |
. . . . . 6
⊢ (𝑧 ∈ 𝐴 → (𝑅 Se 𝐴 → (𝐴 ∩ (◡𝑅 “ {𝑧})) ∈ V)) |
5 | 4 | adantl 275 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝑅 Se 𝐴 → (𝐴 ∩ (◡𝑅 “ {𝑧})) ∈ V)) |
6 | | imaeq2 4925 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐴 ∩ (◡𝑅 “ {𝑧})) → (𝐻 “ 𝑥) = (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑧})))) |
7 | 6 | eleq1d 2226 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐴 ∩ (◡𝑅 “ {𝑧})) → ((𝐻 “ 𝑥) ∈ V ↔ (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑧}))) ∈ V)) |
8 | 7 | imbi2d 229 |
. . . . . . . . 9
⊢ (𝑥 = (𝐴 ∩ (◡𝑅 “ {𝑧})) → ((𝜑 → (𝐻 “ 𝑥) ∈ V) ↔ (𝜑 → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑧}))) ∈ V))) |
9 | | isofrlem.2 |
. . . . . . . . 9
⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V) |
10 | 8, 9 | vtoclg 2772 |
. . . . . . . 8
⊢ ((𝐴 ∩ (◡𝑅 “ {𝑧})) ∈ V → (𝜑 → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑧}))) ∈ V)) |
11 | 10 | com12 30 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 ∩ (◡𝑅 “ {𝑧})) ∈ V → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑧}))) ∈ V)) |
12 | 11 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐴 ∩ (◡𝑅 “ {𝑧})) ∈ V → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑧}))) ∈ V)) |
13 | | isofrlem.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)) |
14 | | isoini 5769 |
. . . . . . . 8
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑧 ∈ 𝐴) → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑧}))) = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑧)}))) |
15 | 13, 14 | sylan 281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑧}))) = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑧)}))) |
16 | 15 | eleq1d 2226 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑧}))) ∈ V ↔ (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑧)})) ∈ V)) |
17 | 12, 16 | sylibd 148 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐴 ∩ (◡𝑅 “ {𝑧})) ∈ V → (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑧)})) ∈ V)) |
18 | 5, 17 | syld 45 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝑅 Se 𝐴 → (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑧)})) ∈ V)) |
19 | 18 | ralrimdva 2537 |
. . 3
⊢ (𝜑 → (𝑅 Se 𝐴 → ∀𝑧 ∈ 𝐴 (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑧)})) ∈ V)) |
20 | | isof1o 5758 |
. . . . 5
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵) |
21 | | f1ofn 5416 |
. . . . 5
⊢ (𝐻:𝐴–1-1-onto→𝐵 → 𝐻 Fn 𝐴) |
22 | | sneq 3571 |
. . . . . . . . 9
⊢ (𝑦 = (𝐻‘𝑧) → {𝑦} = {(𝐻‘𝑧)}) |
23 | 22 | imaeq2d 4929 |
. . . . . . . 8
⊢ (𝑦 = (𝐻‘𝑧) → (◡𝑆 “ {𝑦}) = (◡𝑆 “ {(𝐻‘𝑧)})) |
24 | 23 | ineq2d 3308 |
. . . . . . 7
⊢ (𝑦 = (𝐻‘𝑧) → (𝐵 ∩ (◡𝑆 “ {𝑦})) = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑧)}))) |
25 | 24 | eleq1d 2226 |
. . . . . 6
⊢ (𝑦 = (𝐻‘𝑧) → ((𝐵 ∩ (◡𝑆 “ {𝑦})) ∈ V ↔ (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑧)})) ∈ V)) |
26 | 25 | ralrn 5606 |
. . . . 5
⊢ (𝐻 Fn 𝐴 → (∀𝑦 ∈ ran 𝐻(𝐵 ∩ (◡𝑆 “ {𝑦})) ∈ V ↔ ∀𝑧 ∈ 𝐴 (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑧)})) ∈ V)) |
27 | 13, 20, 21, 26 | 4syl 18 |
. . . 4
⊢ (𝜑 → (∀𝑦 ∈ ran 𝐻(𝐵 ∩ (◡𝑆 “ {𝑦})) ∈ V ↔ ∀𝑧 ∈ 𝐴 (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑧)})) ∈ V)) |
28 | | f1ofo 5422 |
. . . . . 6
⊢ (𝐻:𝐴–1-1-onto→𝐵 → 𝐻:𝐴–onto→𝐵) |
29 | | forn 5396 |
. . . . . 6
⊢ (𝐻:𝐴–onto→𝐵 → ran 𝐻 = 𝐵) |
30 | 13, 20, 28, 29 | 4syl 18 |
. . . . 5
⊢ (𝜑 → ran 𝐻 = 𝐵) |
31 | 30 | raleqdv 2658 |
. . . 4
⊢ (𝜑 → (∀𝑦 ∈ ran 𝐻(𝐵 ∩ (◡𝑆 “ {𝑦})) ∈ V ↔ ∀𝑦 ∈ 𝐵 (𝐵 ∩ (◡𝑆 “ {𝑦})) ∈ V)) |
32 | 27, 31 | bitr3d 189 |
. . 3
⊢ (𝜑 → (∀𝑧 ∈ 𝐴 (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑧)})) ∈ V ↔ ∀𝑦 ∈ 𝐵 (𝐵 ∩ (◡𝑆 “ {𝑦})) ∈ V)) |
33 | 19, 32 | sylibd 148 |
. 2
⊢ (𝜑 → (𝑅 Se 𝐴 → ∀𝑦 ∈ 𝐵 (𝐵 ∩ (◡𝑆 “ {𝑦})) ∈ V)) |
34 | | dfse2 4960 |
. 2
⊢ (𝑆 Se 𝐵 ↔ ∀𝑦 ∈ 𝐵 (𝐵 ∩ (◡𝑆 “ {𝑦})) ∈ V) |
35 | 33, 34 | syl6ibr 161 |
1
⊢ (𝜑 → (𝑅 Se 𝐴 → 𝑆 Se 𝐵)) |