Step |
Hyp |
Ref |
Expression |
1 |
|
djuen |
⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ) → ( 𝐴 ⊔ 𝐶 ) ≈ ( 𝐵 ⊔ 𝐷 ) ) |
2 |
1
|
3adant3 |
⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( 𝐴 ⊔ 𝐶 ) ≈ ( 𝐵 ⊔ 𝐷 ) ) |
3 |
|
relen |
⊢ Rel ≈ |
4 |
3
|
brrelex2i |
⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ∈ V ) |
5 |
3
|
brrelex2i |
⊢ ( 𝐶 ≈ 𝐷 → 𝐷 ∈ V ) |
6 |
|
id |
⊢ ( ( 𝐵 ∩ 𝐷 ) = ∅ → ( 𝐵 ∩ 𝐷 ) = ∅ ) |
7 |
|
endjudisj |
⊢ ( ( 𝐵 ∈ V ∧ 𝐷 ∈ V ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( 𝐵 ⊔ 𝐷 ) ≈ ( 𝐵 ∪ 𝐷 ) ) |
8 |
4 5 6 7
|
syl3an |
⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( 𝐵 ⊔ 𝐷 ) ≈ ( 𝐵 ∪ 𝐷 ) ) |
9 |
|
entr |
⊢ ( ( ( 𝐴 ⊔ 𝐶 ) ≈ ( 𝐵 ⊔ 𝐷 ) ∧ ( 𝐵 ⊔ 𝐷 ) ≈ ( 𝐵 ∪ 𝐷 ) ) → ( 𝐴 ⊔ 𝐶 ) ≈ ( 𝐵 ∪ 𝐷 ) ) |
10 |
2 8 9
|
syl2anc |
⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( 𝐴 ⊔ 𝐶 ) ≈ ( 𝐵 ∪ 𝐷 ) ) |