Step |
Hyp |
Ref |
Expression |
1 |
|
ne0i |
⊢ ( 𝐴 ∈ 𝑇 → 𝑇 ≠ ∅ ) |
2 |
|
tskwun |
⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑇 ≠ ∅ ) → 𝑇 ∈ WUni ) |
3 |
2
|
3expa |
⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝑇 ≠ ∅ ) → 𝑇 ∈ WUni ) |
4 |
1 3
|
sylan2 |
⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ) → 𝑇 ∈ WUni ) |
5 |
4
|
3adant3 |
⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → 𝑇 ∈ WUni ) |
6 |
|
simp2 |
⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → 𝐴 ∈ 𝑇 ) |
7 |
|
simp3 |
⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → 𝐵 ∈ 𝑇 ) |
8 |
5 6 7
|
wunxp |
⊢ ( ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → ( 𝐴 × 𝐵 ) ∈ 𝑇 ) |