Proof of Theorem en3lplem2VD
Step | Hyp | Ref
| Expression |
1 | | idn1 41724 |
. . . . . . 7
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ▶ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ) |
2 | | idn3 41765 |
. . . . . . 7
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 ∈ {𝐴, 𝐵, 𝐶} , 𝑥 = 𝐴 ▶ 𝑥 = 𝐴 ) |
3 | | en3lplem1VD 41993 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 = 𝐴 → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥))) |
4 | 1, 2, 3 | e13 41898 |
. . . . . 6
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 ∈ {𝐴, 𝐵, 𝐶} , 𝑥 = 𝐴 ▶ ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥) ) |
5 | 4 | in3 41759 |
. . . . 5
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 ∈ {𝐴, 𝐵, 𝐶} ▶ (𝑥 = 𝐴 → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)) ) |
6 | | 3anrot 1101 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ↔ (𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ∧ 𝐴 ∈ 𝐵)) |
7 | 1, 6 | e1bi 41779 |
. . . . . . . 8
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ▶ (𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ∧ 𝐴 ∈ 𝐵) ) |
8 | | idn3 41765 |
. . . . . . . 8
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 ∈ {𝐴, 𝐵, 𝐶} , 𝑥 = 𝐵 ▶ 𝑥 = 𝐵 ) |
9 | | en3lplem1VD 41993 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ∧ 𝐴 ∈ 𝐵) → (𝑥 = 𝐵 → ∃𝑦(𝑦 ∈ {𝐵, 𝐶, 𝐴} ∧ 𝑦 ∈ 𝑥))) |
10 | 7, 8, 9 | e13 41898 |
. . . . . . 7
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 ∈ {𝐴, 𝐵, 𝐶} , 𝑥 = 𝐵 ▶ ∃𝑦(𝑦 ∈ {𝐵, 𝐶, 𝐴} ∧ 𝑦 ∈ 𝑥) ) |
11 | | tprot 4641 |
. . . . . . . . . 10
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴} |
12 | 11 | eleq2i 2824 |
. . . . . . . . 9
⊢ (𝑦 ∈ {𝐴, 𝐵, 𝐶} ↔ 𝑦 ∈ {𝐵, 𝐶, 𝐴}) |
13 | 12 | anbi1i 627 |
. . . . . . . 8
⊢ ((𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥) ↔ (𝑦 ∈ {𝐵, 𝐶, 𝐴} ∧ 𝑦 ∈ 𝑥)) |
14 | 13 | exbii 1854 |
. . . . . . 7
⊢
(∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥) ↔ ∃𝑦(𝑦 ∈ {𝐵, 𝐶, 𝐴} ∧ 𝑦 ∈ 𝑥)) |
15 | 10, 14 | e3bir 41889 |
. . . . . 6
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 ∈ {𝐴, 𝐵, 𝐶} , 𝑥 = 𝐵 ▶ ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥) ) |
16 | 15 | in3 41759 |
. . . . 5
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 ∈ {𝐴, 𝐵, 𝐶} ▶ (𝑥 = 𝐵 → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)) ) |
17 | | jao 960 |
. . . . 5
⊢ ((𝑥 = 𝐴 → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)) → ((𝑥 = 𝐵 → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)) → ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)))) |
18 | 5, 16, 17 | e22 41821 |
. . . 4
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 ∈ {𝐴, 𝐵, 𝐶} ▶ ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)) ) |
19 | | 3anrot 1101 |
. . . . . . . 8
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴)) |
20 | 1, 19 | e1bir 41780 |
. . . . . . 7
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ▶ (𝐶 ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) ) |
21 | | idn3 41765 |
. . . . . . 7
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 ∈ {𝐴, 𝐵, 𝐶} , 𝑥 = 𝐶 ▶ 𝑥 = 𝐶 ) |
22 | | en3lplem1VD 41993 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → (𝑥 = 𝐶 → ∃𝑦(𝑦 ∈ {𝐶, 𝐴, 𝐵} ∧ 𝑦 ∈ 𝑥))) |
23 | 20, 21, 22 | e13 41898 |
. . . . . 6
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 ∈ {𝐴, 𝐵, 𝐶} , 𝑥 = 𝐶 ▶ ∃𝑦(𝑦 ∈ {𝐶, 𝐴, 𝐵} ∧ 𝑦 ∈ 𝑥) ) |
24 | | tprot 4641 |
. . . . . . . . 9
⊢ {𝐶, 𝐴, 𝐵} = {𝐴, 𝐵, 𝐶} |
25 | 24 | eleq2i 2824 |
. . . . . . . 8
⊢ (𝑦 ∈ {𝐶, 𝐴, 𝐵} ↔ 𝑦 ∈ {𝐴, 𝐵, 𝐶}) |
26 | 25 | anbi1i 627 |
. . . . . . 7
⊢ ((𝑦 ∈ {𝐶, 𝐴, 𝐵} ∧ 𝑦 ∈ 𝑥) ↔ (𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)) |
27 | 26 | exbii 1854 |
. . . . . 6
⊢
(∃𝑦(𝑦 ∈ {𝐶, 𝐴, 𝐵} ∧ 𝑦 ∈ 𝑥) ↔ ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)) |
28 | 23, 27 | e3bi 41888 |
. . . . 5
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 ∈ {𝐴, 𝐵, 𝐶} , 𝑥 = 𝐶 ▶ ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥) ) |
29 | 28 | in3 41759 |
. . . 4
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 ∈ {𝐴, 𝐵, 𝐶} ▶ (𝑥 = 𝐶 → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)) ) |
30 | | idn2 41763 |
. . . . . . 7
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 ∈ {𝐴, 𝐵, 𝐶} ▶ 𝑥 ∈ {𝐴, 𝐵, 𝐶} ) |
31 | | dftp2 4581 |
. . . . . . . 8
⊢ {𝐴, 𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)} |
32 | 31 | eleq2i 2824 |
. . . . . . 7
⊢ (𝑥 ∈ {𝐴, 𝐵, 𝐶} ↔ 𝑥 ∈ {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)}) |
33 | 30, 32 | e2bi 41782 |
. . . . . 6
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 ∈ {𝐴, 𝐵, 𝐶} ▶ 𝑥 ∈ {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)} ) |
34 | | abid 2720 |
. . . . . 6
⊢ (𝑥 ∈ {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)} ↔ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)) |
35 | 33, 34 | e2bi 41782 |
. . . . 5
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 ∈ {𝐴, 𝐵, 𝐶} ▶ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶) ) |
36 | | df-3or 1089 |
. . . . 5
⊢ ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶) ↔ ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ∨ 𝑥 = 𝐶)) |
37 | 35, 36 | e2bi 41782 |
. . . 4
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 ∈ {𝐴, 𝐵, 𝐶} ▶ ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ∨ 𝑥 = 𝐶) ) |
38 | | jao 960 |
. . . 4
⊢ (((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)) → ((𝑥 = 𝐶 → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)) → (((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ∨ 𝑥 = 𝐶) → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)))) |
39 | 18, 29, 37, 38 | e222 41786 |
. . 3
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) , 𝑥 ∈ {𝐴, 𝐵, 𝐶} ▶ ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥) ) |
40 | 39 | in2 41755 |
. 2
⊢ ( (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) ▶ (𝑥 ∈ {𝐴, 𝐵, 𝐶} → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)) ) |
41 | 40 | in1 41721 |
1
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 ∈ {𝐴, 𝐵, 𝐶} → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥))) |