Step |
Hyp |
Ref |
Expression |
1 |
|
wun0.1 |
⊢ ( 𝜑 → 𝑈 ∈ WUni ) |
2 |
|
wunop.2 |
⊢ ( 𝜑 → 𝐴 ∈ 𝑈 ) |
3 |
|
wunco.3 |
⊢ ( 𝜑 → 𝐵 ∈ 𝑈 ) |
4 |
1 3
|
wundm |
⊢ ( 𝜑 → dom 𝐵 ∈ 𝑈 ) |
5 |
|
dmcoss |
⊢ dom ( 𝐴 ∘ 𝐵 ) ⊆ dom 𝐵 |
6 |
5
|
a1i |
⊢ ( 𝜑 → dom ( 𝐴 ∘ 𝐵 ) ⊆ dom 𝐵 ) |
7 |
1 4 6
|
wunss |
⊢ ( 𝜑 → dom ( 𝐴 ∘ 𝐵 ) ∈ 𝑈 ) |
8 |
1 2
|
wunrn |
⊢ ( 𝜑 → ran 𝐴 ∈ 𝑈 ) |
9 |
|
rncoss |
⊢ ran ( 𝐴 ∘ 𝐵 ) ⊆ ran 𝐴 |
10 |
9
|
a1i |
⊢ ( 𝜑 → ran ( 𝐴 ∘ 𝐵 ) ⊆ ran 𝐴 ) |
11 |
1 8 10
|
wunss |
⊢ ( 𝜑 → ran ( 𝐴 ∘ 𝐵 ) ∈ 𝑈 ) |
12 |
1 7 11
|
wunxp |
⊢ ( 𝜑 → ( dom ( 𝐴 ∘ 𝐵 ) × ran ( 𝐴 ∘ 𝐵 ) ) ∈ 𝑈 ) |
13 |
|
relco |
⊢ Rel ( 𝐴 ∘ 𝐵 ) |
14 |
|
relssdmrn |
⊢ ( Rel ( 𝐴 ∘ 𝐵 ) → ( 𝐴 ∘ 𝐵 ) ⊆ ( dom ( 𝐴 ∘ 𝐵 ) × ran ( 𝐴 ∘ 𝐵 ) ) ) |
15 |
13 14
|
mp1i |
⊢ ( 𝜑 → ( 𝐴 ∘ 𝐵 ) ⊆ ( dom ( 𝐴 ∘ 𝐵 ) × ran ( 𝐴 ∘ 𝐵 ) ) ) |
16 |
1 12 15
|
wunss |
⊢ ( 𝜑 → ( 𝐴 ∘ 𝐵 ) ∈ 𝑈 ) |