Proof of Theorem en3lplem1VD
Step | Hyp | Ref
| Expression |
1 | | idn1 38790 |
. . . . . . 7
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ▶ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ) |
2 | | simp3 1063 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐴) |
3 | 1, 2 | e1a 38852 |
. . . . . 6
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ▶ 𝐶 ∈ 𝐴 ) |
4 | | tpid3g 4305 |
. . . . . 6
⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ {𝐴, 𝐵, 𝐶}) |
5 | 3, 4 | e1a 38852 |
. . . . 5
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ▶ 𝐶 ∈ {𝐴, 𝐵, 𝐶} ) |
6 | | idn2 38838 |
. . . . . 6
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 = 𝐴 ▶ 𝑥 = 𝐴 ) |
7 | | eleq2 2690 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝐶 ∈ 𝑥 ↔ 𝐶 ∈ 𝐴)) |
8 | 7 | biimprd 238 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝑥)) |
9 | 6, 3, 8 | e21 38957 |
. . . . 5
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 = 𝐴 ▶ 𝐶 ∈ 𝑥 ) |
10 | | pm3.2 463 |
. . . . 5
⊢ (𝐶 ∈ {𝐴, 𝐵, 𝐶} → (𝐶 ∈ 𝑥 → (𝐶 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝐶 ∈ 𝑥))) |
11 | 5, 9, 10 | e12 38951 |
. . . 4
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 = 𝐴 ▶ (𝐶 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝐶 ∈ 𝑥) ) |
12 | | elex22 3217 |
. . . 4
⊢ ((𝐶 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝐶 ∈ 𝑥) → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)) |
13 | 11, 12 | e2 38856 |
. . 3
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 = 𝐴 ▶ ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥) ) |
14 | 13 | in2 38830 |
. 2
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ▶ (𝑥 = 𝐴 → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)) ) |
15 | 14 | in1 38787 |
1
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 = 𝐴 → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥))) |