Step | Hyp | Ref
| Expression |
1 | | ssel 3141 |
. . . . . . 7
⊢ (𝐵 ⊆ 𝐴 → (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)) |
2 | | ssel 3141 |
. . . . . . 7
⊢ (𝐵 ⊆ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐴)) |
3 | | ssel 3141 |
. . . . . . 7
⊢ (𝐵 ⊆ 𝐴 → (𝑧 ∈ 𝐵 → 𝑧 ∈ 𝐴)) |
4 | 1, 2, 3 | 3anim123d 1314 |
. . . . . 6
⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴))) |
5 | 4 | adantl 275 |
. . . . 5
⊢ (( E We
𝐴 ∧ 𝐵 ⊆ 𝐴) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴))) |
6 | 5 | imdistani 443 |
. . . 4
⊢ ((( E We
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (( E We 𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴))) |
7 | | wetrep 4343 |
. . . . . 6
⊢ (( E We
𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧)) |
8 | 7 | adantlr 474 |
. . . . 5
⊢ ((( E We
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧)) |
9 | | epel 4275 |
. . . . . 6
⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦) |
10 | | epel 4275 |
. . . . . 6
⊢ (𝑦 E 𝑧 ↔ 𝑦 ∈ 𝑧) |
11 | 9, 10 | anbi12i 457 |
. . . . 5
⊢ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) ↔ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧)) |
12 | | epel 4275 |
. . . . 5
⊢ (𝑥 E 𝑧 ↔ 𝑥 ∈ 𝑧) |
13 | 8, 11, 12 | 3imtr4g 204 |
. . . 4
⊢ ((( E We
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧)) |
14 | 6, 13 | syl 14 |
. . 3
⊢ ((( E We
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧)) |
15 | 14 | ralrimivvva 2553 |
. 2
⊢ (( E We
𝐴 ∧ 𝐵 ⊆ 𝐴) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧)) |
16 | | zfregfr 4556 |
. . 3
⊢ E Fr
𝐵 |
17 | | df-wetr 4317 |
. . 3
⊢ ( E We
𝐵 ↔ ( E Fr 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧))) |
18 | 16, 17 | mpbiran 935 |
. 2
⊢ ( E We
𝐵 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧)) |
19 | 15, 18 | sylibr 133 |
1
⊢ (( E We
𝐴 ∧ 𝐵 ⊆ 𝐴) → E We 𝐵) |