Proof of Theorem gruima
Step | Hyp | Ref
| Expression |
1 | | simpl2 1188 |
. . . 4
⊢ (((𝑈 ∈ Univ ∧ Fun 𝐹 ∧ (𝐹 “ 𝐴) ⊆ 𝑈) ∧ 𝐴 ∈ 𝑈) → Fun 𝐹) |
2 | | funrel 6374 |
. . . 4
⊢ (Fun
𝐹 → Rel 𝐹) |
3 | | resres 5868 |
. . . . . . 7
⊢ ((𝐹 ↾ dom 𝐹) ↾ 𝐴) = (𝐹 ↾ (dom 𝐹 ∩ 𝐴)) |
4 | | resdm 5899 |
. . . . . . . 8
⊢ (Rel
𝐹 → (𝐹 ↾ dom 𝐹) = 𝐹) |
5 | 4 | reseq1d 5854 |
. . . . . . 7
⊢ (Rel
𝐹 → ((𝐹 ↾ dom 𝐹) ↾ 𝐴) = (𝐹 ↾ 𝐴)) |
6 | 3, 5 | syl5eqr 2872 |
. . . . . 6
⊢ (Rel
𝐹 → (𝐹 ↾ (dom 𝐹 ∩ 𝐴)) = (𝐹 ↾ 𝐴)) |
7 | 6 | rneqd 5810 |
. . . . 5
⊢ (Rel
𝐹 → ran (𝐹 ↾ (dom 𝐹 ∩ 𝐴)) = ran (𝐹 ↾ 𝐴)) |
8 | | df-ima 5570 |
. . . . 5
⊢ (𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴) |
9 | 7, 8 | syl6reqr 2877 |
. . . 4
⊢ (Rel
𝐹 → (𝐹 “ 𝐴) = ran (𝐹 ↾ (dom 𝐹 ∩ 𝐴))) |
10 | 1, 2, 9 | 3syl 18 |
. . 3
⊢ (((𝑈 ∈ Univ ∧ Fun 𝐹 ∧ (𝐹 “ 𝐴) ⊆ 𝑈) ∧ 𝐴 ∈ 𝑈) → (𝐹 “ 𝐴) = ran (𝐹 ↾ (dom 𝐹 ∩ 𝐴))) |
11 | | simpl1 1187 |
. . . 4
⊢ (((𝑈 ∈ Univ ∧ Fun 𝐹 ∧ (𝐹 “ 𝐴) ⊆ 𝑈) ∧ 𝐴 ∈ 𝑈) → 𝑈 ∈ Univ) |
12 | | simpr 487 |
. . . . 5
⊢ (((𝑈 ∈ Univ ∧ Fun 𝐹 ∧ (𝐹 “ 𝐴) ⊆ 𝑈) ∧ 𝐴 ∈ 𝑈) → 𝐴 ∈ 𝑈) |
13 | | inss2 4208 |
. . . . . 6
⊢ (dom
𝐹 ∩ 𝐴) ⊆ 𝐴 |
14 | 13 | a1i 11 |
. . . . 5
⊢ (((𝑈 ∈ Univ ∧ Fun 𝐹 ∧ (𝐹 “ 𝐴) ⊆ 𝑈) ∧ 𝐴 ∈ 𝑈) → (dom 𝐹 ∩ 𝐴) ⊆ 𝐴) |
15 | | gruss 10220 |
. . . . 5
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ (dom 𝐹 ∩ 𝐴) ⊆ 𝐴) → (dom 𝐹 ∩ 𝐴) ∈ 𝑈) |
16 | 11, 12, 14, 15 | syl3anc 1367 |
. . . 4
⊢ (((𝑈 ∈ Univ ∧ Fun 𝐹 ∧ (𝐹 “ 𝐴) ⊆ 𝑈) ∧ 𝐴 ∈ 𝑈) → (dom 𝐹 ∩ 𝐴) ∈ 𝑈) |
17 | | funforn 6599 |
. . . . . . . 8
⊢ (Fun
𝐹 ↔ 𝐹:dom 𝐹–onto→ran 𝐹) |
18 | | fof 6592 |
. . . . . . . 8
⊢ (𝐹:dom 𝐹–onto→ran 𝐹 → 𝐹:dom 𝐹⟶ran 𝐹) |
19 | 17, 18 | sylbi 219 |
. . . . . . 7
⊢ (Fun
𝐹 → 𝐹:dom 𝐹⟶ran 𝐹) |
20 | | inss1 4207 |
. . . . . . 7
⊢ (dom
𝐹 ∩ 𝐴) ⊆ dom 𝐹 |
21 | | fssres 6546 |
. . . . . . 7
⊢ ((𝐹:dom 𝐹⟶ran 𝐹 ∧ (dom 𝐹 ∩ 𝐴) ⊆ dom 𝐹) → (𝐹 ↾ (dom 𝐹 ∩ 𝐴)):(dom 𝐹 ∩ 𝐴)⟶ran 𝐹) |
22 | 19, 20, 21 | sylancl 588 |
. . . . . 6
⊢ (Fun
𝐹 → (𝐹 ↾ (dom 𝐹 ∩ 𝐴)):(dom 𝐹 ∩ 𝐴)⟶ran 𝐹) |
23 | | ffn 6516 |
. . . . . 6
⊢ ((𝐹 ↾ (dom 𝐹 ∩ 𝐴)):(dom 𝐹 ∩ 𝐴)⟶ran 𝐹 → (𝐹 ↾ (dom 𝐹 ∩ 𝐴)) Fn (dom 𝐹 ∩ 𝐴)) |
24 | 1, 22, 23 | 3syl 18 |
. . . . 5
⊢ (((𝑈 ∈ Univ ∧ Fun 𝐹 ∧ (𝐹 “ 𝐴) ⊆ 𝑈) ∧ 𝐴 ∈ 𝑈) → (𝐹 ↾ (dom 𝐹 ∩ 𝐴)) Fn (dom 𝐹 ∩ 𝐴)) |
25 | | simpl3 1189 |
. . . . . 6
⊢ (((𝑈 ∈ Univ ∧ Fun 𝐹 ∧ (𝐹 “ 𝐴) ⊆ 𝑈) ∧ 𝐴 ∈ 𝑈) → (𝐹 “ 𝐴) ⊆ 𝑈) |
26 | 10, 25 | eqsstrrd 4008 |
. . . . 5
⊢ (((𝑈 ∈ Univ ∧ Fun 𝐹 ∧ (𝐹 “ 𝐴) ⊆ 𝑈) ∧ 𝐴 ∈ 𝑈) → ran (𝐹 ↾ (dom 𝐹 ∩ 𝐴)) ⊆ 𝑈) |
27 | | df-f 6361 |
. . . . 5
⊢ ((𝐹 ↾ (dom 𝐹 ∩ 𝐴)):(dom 𝐹 ∩ 𝐴)⟶𝑈 ↔ ((𝐹 ↾ (dom 𝐹 ∩ 𝐴)) Fn (dom 𝐹 ∩ 𝐴) ∧ ran (𝐹 ↾ (dom 𝐹 ∩ 𝐴)) ⊆ 𝑈)) |
28 | 24, 26, 27 | sylanbrc 585 |
. . . 4
⊢ (((𝑈 ∈ Univ ∧ Fun 𝐹 ∧ (𝐹 “ 𝐴) ⊆ 𝑈) ∧ 𝐴 ∈ 𝑈) → (𝐹 ↾ (dom 𝐹 ∩ 𝐴)):(dom 𝐹 ∩ 𝐴)⟶𝑈) |
29 | | grurn 10225 |
. . . 4
⊢ ((𝑈 ∈ Univ ∧ (dom 𝐹 ∩ 𝐴) ∈ 𝑈 ∧ (𝐹 ↾ (dom 𝐹 ∩ 𝐴)):(dom 𝐹 ∩ 𝐴)⟶𝑈) → ran (𝐹 ↾ (dom 𝐹 ∩ 𝐴)) ∈ 𝑈) |
30 | 11, 16, 28, 29 | syl3anc 1367 |
. . 3
⊢ (((𝑈 ∈ Univ ∧ Fun 𝐹 ∧ (𝐹 “ 𝐴) ⊆ 𝑈) ∧ 𝐴 ∈ 𝑈) → ran (𝐹 ↾ (dom 𝐹 ∩ 𝐴)) ∈ 𝑈) |
31 | 10, 30 | eqeltrd 2915 |
. 2
⊢ (((𝑈 ∈ Univ ∧ Fun 𝐹 ∧ (𝐹 “ 𝐴) ⊆ 𝑈) ∧ 𝐴 ∈ 𝑈) → (𝐹 “ 𝐴) ∈ 𝑈) |
32 | 31 | ex 415 |
1
⊢ ((𝑈 ∈ Univ ∧ Fun 𝐹 ∧ (𝐹 “ 𝐴) ⊆ 𝑈) → (𝐴 ∈ 𝑈 → (𝐹 “ 𝐴) ∈ 𝑈)) |