Proof of Theorem en3lplem1VD
| Step | Hyp | Ref
| Expression |
| 1 | | idn1 44594 |
. . . . . . 7
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ▶ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ) |
| 2 | | simp3 1139 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐴) |
| 3 | 1, 2 | e1a 44647 |
. . . . . 6
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ▶ 𝐶 ∈ 𝐴 ) |
| 4 | | tpid3g 4772 |
. . . . . 6
⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ {𝐴, 𝐵, 𝐶}) |
| 5 | 3, 4 | e1a 44647 |
. . . . 5
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ▶ 𝐶 ∈ {𝐴, 𝐵, 𝐶} ) |
| 6 | | idn2 44633 |
. . . . . 6
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 = 𝐴 ▶ 𝑥 = 𝐴 ) |
| 7 | | eleq2 2830 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝐶 ∈ 𝑥 ↔ 𝐶 ∈ 𝐴)) |
| 8 | 7 | biimprd 248 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝑥)) |
| 9 | 6, 3, 8 | e21 44750 |
. . . . 5
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 = 𝐴 ▶ 𝐶 ∈ 𝑥 ) |
| 10 | | pm3.2 469 |
. . . . 5
⊢ (𝐶 ∈ {𝐴, 𝐵, 𝐶} → (𝐶 ∈ 𝑥 → (𝐶 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝐶 ∈ 𝑥))) |
| 11 | 5, 9, 10 | e12 44744 |
. . . 4
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 = 𝐴 ▶ (𝐶 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝐶 ∈ 𝑥) ) |
| 12 | | elex22 3506 |
. . . 4
⊢ ((𝐶 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝐶 ∈ 𝑥) → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)) |
| 13 | 11, 12 | e2 44651 |
. . 3
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 = 𝐴 ▶ ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥) ) |
| 14 | 13 | in2 44625 |
. 2
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ▶ (𝑥 = 𝐴 → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)) ) |
| 15 | 14 | in1 44591 |
1
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 = 𝐴 → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥))) |