Step | Hyp | Ref
| Expression |
1 | | bren 8520 |
. . . . 5
⊢ (𝐵 ≈ 𝐴 ↔ ∃𝑦 𝑦:𝐵–1-1-onto→𝐴) |
2 | | f1ofo 6624 |
. . . . . . . . 9
⊢ (𝑦:𝐵–1-1-onto→𝐴 → 𝑦:𝐵–onto→𝐴) |
3 | | simp3l 1197 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ∧ (𝑦:𝐵–onto→𝐴 ∧ 𝐴 ⊆ 𝑈)) → 𝑦:𝐵–onto→𝐴) |
4 | | forn 6595 |
. . . . . . . . . . . . 13
⊢ (𝑦:𝐵–onto→𝐴 → ran 𝑦 = 𝐴) |
5 | 3, 4 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ∧ (𝑦:𝐵–onto→𝐴 ∧ 𝐴 ⊆ 𝑈)) → ran 𝑦 = 𝐴) |
6 | | fof 6592 |
. . . . . . . . . . . . . 14
⊢ (𝑦:𝐵–onto→𝐴 → 𝑦:𝐵⟶𝐴) |
7 | | fss 6529 |
. . . . . . . . . . . . . 14
⊢ ((𝑦:𝐵⟶𝐴 ∧ 𝐴 ⊆ 𝑈) → 𝑦:𝐵⟶𝑈) |
8 | 6, 7 | sylan 582 |
. . . . . . . . . . . . 13
⊢ ((𝑦:𝐵–onto→𝐴 ∧ 𝐴 ⊆ 𝑈) → 𝑦:𝐵⟶𝑈) |
9 | | grurn 10225 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ∧ 𝑦:𝐵⟶𝑈) → ran 𝑦 ∈ 𝑈) |
10 | 8, 9 | syl3an3 1161 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ∧ (𝑦:𝐵–onto→𝐴 ∧ 𝐴 ⊆ 𝑈)) → ran 𝑦 ∈ 𝑈) |
11 | 5, 10 | eqeltrrd 2916 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ∧ (𝑦:𝐵–onto→𝐴 ∧ 𝐴 ⊆ 𝑈)) → 𝐴 ∈ 𝑈) |
12 | 11 | 3expia 1117 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈) → ((𝑦:𝐵–onto→𝐴 ∧ 𝐴 ⊆ 𝑈) → 𝐴 ∈ 𝑈)) |
13 | 12 | expd 418 |
. . . . . . . . 9
⊢ ((𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈) → (𝑦:𝐵–onto→𝐴 → (𝐴 ⊆ 𝑈 → 𝐴 ∈ 𝑈))) |
14 | 2, 13 | syl5 34 |
. . . . . . . 8
⊢ ((𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈) → (𝑦:𝐵–1-1-onto→𝐴 → (𝐴 ⊆ 𝑈 → 𝐴 ∈ 𝑈))) |
15 | 14 | exlimdv 1934 |
. . . . . . 7
⊢ ((𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈) → (∃𝑦 𝑦:𝐵–1-1-onto→𝐴 → (𝐴 ⊆ 𝑈 → 𝐴 ∈ 𝑈))) |
16 | 15 | com3r 87 |
. . . . . 6
⊢ (𝐴 ⊆ 𝑈 → ((𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈) → (∃𝑦 𝑦:𝐵–1-1-onto→𝐴 → 𝐴 ∈ 𝑈))) |
17 | 16 | expdimp 455 |
. . . . 5
⊢ ((𝐴 ⊆ 𝑈 ∧ 𝑈 ∈ Univ) → (𝐵 ∈ 𝑈 → (∃𝑦 𝑦:𝐵–1-1-onto→𝐴 → 𝐴 ∈ 𝑈))) |
18 | 1, 17 | syl7bi 257 |
. . . 4
⊢ ((𝐴 ⊆ 𝑈 ∧ 𝑈 ∈ Univ) → (𝐵 ∈ 𝑈 → (𝐵 ≈ 𝐴 → 𝐴 ∈ 𝑈))) |
19 | 18 | impd 413 |
. . 3
⊢ ((𝐴 ⊆ 𝑈 ∧ 𝑈 ∈ Univ) → ((𝐵 ∈ 𝑈 ∧ 𝐵 ≈ 𝐴) → 𝐴 ∈ 𝑈)) |
20 | 19 | ancoms 461 |
. 2
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ⊆ 𝑈) → ((𝐵 ∈ 𝑈 ∧ 𝐵 ≈ 𝐴) → 𝐴 ∈ 𝑈)) |
21 | 20 | 3impia 1113 |
1
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ⊆ 𝑈 ∧ (𝐵 ∈ 𝑈 ∧ 𝐵 ≈ 𝐴)) → 𝐴 ∈ 𝑈) |