Proof of Theorem en3lplem1VD
Step | Hyp | Ref
| Expression |
1 | | idn1 37811 |
. . . . . . 7
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ▶ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ) |
2 | | simp3 1056 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐴) |
3 | 1, 2 | e1a 37873 |
. . . . . 6
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ▶ 𝐶 ∈ 𝐴 ) |
4 | | tpid3g 4248 |
. . . . . 6
⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ {𝐴, 𝐵, 𝐶}) |
5 | 3, 4 | e1a 37873 |
. . . . 5
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ▶ 𝐶 ∈ {𝐴, 𝐵, 𝐶} ) |
6 | | idn2 37859 |
. . . . . 6
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 = 𝐴 ▶ 𝑥 = 𝐴 ) |
7 | | eleq2 2677 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝐶 ∈ 𝑥 ↔ 𝐶 ∈ 𝐴)) |
8 | 7 | biimprd 237 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝑥)) |
9 | 6, 3, 8 | e21 37978 |
. . . . 5
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 = 𝐴 ▶ 𝐶 ∈ 𝑥 ) |
10 | | pm3.2 462 |
. . . . 5
⊢ (𝐶 ∈ {𝐴, 𝐵, 𝐶} → (𝐶 ∈ 𝑥 → (𝐶 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝐶 ∈ 𝑥))) |
11 | 5, 9, 10 | e12 37972 |
. . . 4
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 = 𝐴 ▶ (𝐶 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝐶 ∈ 𝑥) ) |
12 | | elex22 3190 |
. . . 4
⊢ ((𝐶 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝐶 ∈ 𝑥) → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)) |
13 | 11, 12 | e2 37877 |
. . 3
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 = 𝐴 ▶ ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥) ) |
14 | 13 | in2 37851 |
. 2
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ▶ (𝑥 = 𝐴 → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)) ) |
15 | 14 | in1 37808 |
1
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 = 𝐴 → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥))) |