Step | Hyp | Ref
| Expression |
1 | | df-res 5050 |
. 2
⊢ (𝑇 ↾ (V ∖ {𝐴})) = (𝑇 ∩ ((V ∖ {𝐴}) × V)) |
2 | | elin 3758 |
. . . 4
⊢ (𝑥 ∈ (𝑇 ∩ ((V ∖ {𝐴}) × V)) ↔ (𝑥 ∈ 𝑇 ∧ 𝑥 ∈ ((V ∖ {𝐴}) × V))) |
3 | | elxp 5055 |
. . . . . 6
⊢ (𝑥 ∈ ((V ∖ {𝐴}) × V) ↔
∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) |
4 | 3 | anbi2i 726 |
. . . . 5
⊢ ((𝑥 ∈ 𝑇 ∧ 𝑥 ∈ ((V ∖ {𝐴}) × V)) ↔ (𝑥 ∈ 𝑇 ∧ ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)))) |
5 | | tpres.t |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 = {〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}) |
6 | 5 | eleq2d 2673 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑇 ↔ 𝑥 ∈ {〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉})) |
7 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
8 | 7 | eltp 4177 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉} ↔ (𝑥 = 〈𝐴, 𝐷〉 ∨ 𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉)) |
9 | | eldifsn 4260 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ (V ∖ {𝐴}) ↔ (𝑎 ∈ V ∧ 𝑎 ≠ 𝐴)) |
10 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 〈𝑎, 𝑏〉 → (𝑥 = 〈𝐴, 𝐷〉 ↔ 〈𝑎, 𝑏〉 = 〈𝐴, 𝐷〉)) |
11 | 10 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 ≠ 𝐴 ∧ 𝑥 = 〈𝑎, 𝑏〉) → (𝑥 = 〈𝐴, 𝐷〉 ↔ 〈𝑎, 𝑏〉 = 〈𝐴, 𝐷〉)) |
12 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑎 ∈ V |
13 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑏 ∈ V |
14 | 12, 13 | opth 4871 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(〈𝑎, 𝑏〉 = 〈𝐴, 𝐷〉 ↔ (𝑎 = 𝐴 ∧ 𝑏 = 𝐷)) |
15 | | eqneqall 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑎 = 𝐴 → (𝑎 ≠ 𝐴 → (𝑏 = 𝐷 → (𝜑 → (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉))))) |
16 | 15 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑎 ≠ 𝐴 → (𝑎 = 𝐴 → (𝑏 = 𝐷 → (𝜑 → (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉))))) |
17 | 16 | impd 446 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 ≠ 𝐴 → ((𝑎 = 𝐴 ∧ 𝑏 = 𝐷) → (𝜑 → (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉)))) |
18 | 14, 17 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 ≠ 𝐴 → (〈𝑎, 𝑏〉 = 〈𝐴, 𝐷〉 → (𝜑 → (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉)))) |
19 | 18 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 ≠ 𝐴 ∧ 𝑥 = 〈𝑎, 𝑏〉) → (〈𝑎, 𝑏〉 = 〈𝐴, 𝐷〉 → (𝜑 → (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉)))) |
20 | 11, 19 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ≠ 𝐴 ∧ 𝑥 = 〈𝑎, 𝑏〉) → (𝑥 = 〈𝐴, 𝐷〉 → (𝜑 → (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉)))) |
21 | 20 | impd 446 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ≠ 𝐴 ∧ 𝑥 = 〈𝑎, 𝑏〉) → ((𝑥 = 〈𝐴, 𝐷〉 ∧ 𝜑) → (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉))) |
22 | 21 | ex 449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ≠ 𝐴 → (𝑥 = 〈𝑎, 𝑏〉 → ((𝑥 = 〈𝐴, 𝐷〉 ∧ 𝜑) → (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉)))) |
23 | 22 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ V ∧ 𝑎 ≠ 𝐴) → (𝑥 = 〈𝑎, 𝑏〉 → ((𝑥 = 〈𝐴, 𝐷〉 ∧ 𝜑) → (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉)))) |
24 | 9, 23 | sylbi 206 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ (V ∖ {𝐴}) → (𝑥 = 〈𝑎, 𝑏〉 → ((𝑥 = 〈𝐴, 𝐷〉 ∧ 𝜑) → (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉)))) |
25 | 24 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V) → (𝑥 = 〈𝑎, 𝑏〉 → ((𝑥 = 〈𝐴, 𝐷〉 ∧ 𝜑) → (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉)))) |
26 | 25 | impcom 445 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) → ((𝑥 = 〈𝐴, 𝐷〉 ∧ 𝜑) → (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉))) |
27 | 26 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 〈𝐴, 𝐷〉 ∧ 𝜑) → ((𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) → (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉))) |
28 | 27 | exlimdvv 1849 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = 〈𝐴, 𝐷〉 ∧ 𝜑) → (∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) → (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉))) |
29 | 28 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 〈𝐴, 𝐷〉 → (𝜑 → (∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) → (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉)))) |
30 | 29 | impd 446 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 〈𝐴, 𝐷〉 → ((𝜑 ∧ ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) → (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉))) |
31 | | orc 399 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 〈𝐵, 𝐸〉 → (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉)) |
32 | 31 | a1d 25 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 〈𝐵, 𝐸〉 → ((𝜑 ∧ ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) → (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉))) |
33 | | olc 398 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 〈𝐶, 𝐹〉 → (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉)) |
34 | 33 | a1d 25 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 〈𝐶, 𝐹〉 → ((𝜑 ∧ ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) → (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉))) |
35 | 30, 32, 34 | 3jaoi 1383 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 〈𝐴, 𝐷〉 ∨ 𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉) → ((𝜑 ∧ ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) → (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉))) |
36 | 8, 35 | sylbi 206 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉} → ((𝜑 ∧ ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) → (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉))) |
37 | 7 | elpr 4146 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉} ↔ (𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉)) |
38 | 36, 37 | syl6ibr 241 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉} → ((𝜑 ∧ ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) → 𝑥 ∈ {〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉})) |
39 | 38 | expd 451 |
. . . . . . . . 9
⊢ (𝑥 ∈ {〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉} → (𝜑 → (∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) → 𝑥 ∈ {〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}))) |
40 | 39 | com12 32 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ {〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉} → (∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) → 𝑥 ∈ {〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}))) |
41 | 6, 40 | sylbid 229 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝑇 → (∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) → 𝑥 ∈ {〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}))) |
42 | 41 | impd 446 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝑇 ∧ ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) → 𝑥 ∈ {〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉})) |
43 | | 3mix2 1224 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 〈𝐵, 𝐸〉 → (𝑥 = 〈𝐴, 𝐷〉 ∨ 𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉)) |
44 | | 3mix3 1225 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 〈𝐶, 𝐹〉 → (𝑥 = 〈𝐴, 𝐷〉 ∨ 𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉)) |
45 | 43, 44 | jaoi 393 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉) → (𝑥 = 〈𝐴, 𝐷〉 ∨ 𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉)) |
46 | 45 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉) ∧ 𝜑) → (𝑥 = 〈𝐴, 𝐷〉 ∨ 𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉)) |
47 | 6, 8 | syl6bb 275 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝑇 ↔ (𝑥 = 〈𝐴, 𝐷〉 ∨ 𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉))) |
48 | 47 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉) ∧ 𝜑) → (𝑥 ∈ 𝑇 ↔ (𝑥 = 〈𝐴, 𝐷〉 ∨ 𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉))) |
49 | 46, 48 | mpbird 246 |
. . . . . . . . . 10
⊢ (((𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉) ∧ 𝜑) → 𝑥 ∈ 𝑇) |
50 | | tpres.b |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
51 | | elex 3185 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈ V) |
53 | | tpres.1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ≠ 𝐴) |
54 | | tpres.e |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐸 ∈ 𝑉) |
55 | | elex 3185 |
. . . . . . . . . . . . . . . 16
⊢ (𝐸 ∈ 𝑉 → 𝐸 ∈ V) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐸 ∈ V) |
57 | 52, 53, 56 | jca31 555 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐵 ∈ V ∧ 𝐵 ≠ 𝐴) ∧ 𝐸 ∈ V)) |
58 | 57 | anim2i 591 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 〈𝐵, 𝐸〉 ∧ 𝜑) → (𝑥 = 〈𝐵, 𝐸〉 ∧ ((𝐵 ∈ V ∧ 𝐵 ≠ 𝐴) ∧ 𝐸 ∈ V))) |
59 | | opeq12 4342 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 = 𝐵 ∧ 𝑏 = 𝐸) → 〈𝑎, 𝑏〉 = 〈𝐵, 𝐸〉) |
60 | 59 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 = 𝐵 ∧ 𝑏 = 𝐸) → (𝑥 = 〈𝑎, 𝑏〉 ↔ 𝑥 = 〈𝐵, 𝐸〉)) |
61 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 𝐵 → (𝑎 ∈ V ↔ 𝐵 ∈ V)) |
62 | | neeq1 2844 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 𝐵 → (𝑎 ≠ 𝐴 ↔ 𝐵 ≠ 𝐴)) |
63 | 61, 62 | anbi12d 743 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝐵 → ((𝑎 ∈ V ∧ 𝑎 ≠ 𝐴) ↔ (𝐵 ∈ V ∧ 𝐵 ≠ 𝐴))) |
64 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = 𝐸 → (𝑏 ∈ V ↔ 𝐸 ∈ V)) |
65 | 63, 64 | bi2anan9 913 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 = 𝐵 ∧ 𝑏 = 𝐸) → (((𝑎 ∈ V ∧ 𝑎 ≠ 𝐴) ∧ 𝑏 ∈ V) ↔ ((𝐵 ∈ V ∧ 𝐵 ≠ 𝐴) ∧ 𝐸 ∈ V))) |
66 | 60, 65 | anbi12d 743 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 = 𝐵 ∧ 𝑏 = 𝐸) → ((𝑥 = 〈𝑎, 𝑏〉 ∧ ((𝑎 ∈ V ∧ 𝑎 ≠ 𝐴) ∧ 𝑏 ∈ V)) ↔ (𝑥 = 〈𝐵, 𝐸〉 ∧ ((𝐵 ∈ V ∧ 𝐵 ≠ 𝐴) ∧ 𝐸 ∈ V)))) |
67 | 66 | spc2egv 3268 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉) → ((𝑥 = 〈𝐵, 𝐸〉 ∧ ((𝐵 ∈ V ∧ 𝐵 ≠ 𝐴) ∧ 𝐸 ∈ V)) → ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ ((𝑎 ∈ V ∧ 𝑎 ≠ 𝐴) ∧ 𝑏 ∈ V)))) |
68 | 50, 54, 67 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑥 = 〈𝐵, 𝐸〉 ∧ ((𝐵 ∈ V ∧ 𝐵 ≠ 𝐴) ∧ 𝐸 ∈ V)) → ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ ((𝑎 ∈ V ∧ 𝑎 ≠ 𝐴) ∧ 𝑏 ∈ V)))) |
69 | 68 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 〈𝐵, 𝐸〉 ∧ 𝜑) → ((𝑥 = 〈𝐵, 𝐸〉 ∧ ((𝐵 ∈ V ∧ 𝐵 ≠ 𝐴) ∧ 𝐸 ∈ V)) → ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ ((𝑎 ∈ V ∧ 𝑎 ≠ 𝐴) ∧ 𝑏 ∈ V)))) |
70 | 58, 69 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 〈𝐵, 𝐸〉 ∧ 𝜑) → ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ ((𝑎 ∈ V ∧ 𝑎 ≠ 𝐴) ∧ 𝑏 ∈ V))) |
71 | | tpres.c |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
72 | | elex 3185 |
. . . . . . . . . . . . . . . 16
⊢ (𝐶 ∈ 𝑉 → 𝐶 ∈ V) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈ V) |
74 | | tpres.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ≠ 𝐴) |
75 | | tpres.f |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹 ∈ 𝑉) |
76 | | elex 3185 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ 𝑉 → 𝐹 ∈ V) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ∈ V) |
78 | 73, 74, 77 | jca31 555 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐶 ∈ V ∧ 𝐶 ≠ 𝐴) ∧ 𝐹 ∈ V)) |
79 | 78 | anim2i 591 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 〈𝐶, 𝐹〉 ∧ 𝜑) → (𝑥 = 〈𝐶, 𝐹〉 ∧ ((𝐶 ∈ V ∧ 𝐶 ≠ 𝐴) ∧ 𝐹 ∈ V))) |
80 | | opeq12 4342 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 = 𝐶 ∧ 𝑏 = 𝐹) → 〈𝑎, 𝑏〉 = 〈𝐶, 𝐹〉) |
81 | 80 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 = 𝐶 ∧ 𝑏 = 𝐹) → (𝑥 = 〈𝑎, 𝑏〉 ↔ 𝑥 = 〈𝐶, 𝐹〉)) |
82 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 𝐶 → (𝑎 ∈ V ↔ 𝐶 ∈ V)) |
83 | | neeq1 2844 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 𝐶 → (𝑎 ≠ 𝐴 ↔ 𝐶 ≠ 𝐴)) |
84 | 82, 83 | anbi12d 743 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝐶 → ((𝑎 ∈ V ∧ 𝑎 ≠ 𝐴) ↔ (𝐶 ∈ V ∧ 𝐶 ≠ 𝐴))) |
85 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = 𝐹 → (𝑏 ∈ V ↔ 𝐹 ∈ V)) |
86 | 84, 85 | bi2anan9 913 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 = 𝐶 ∧ 𝑏 = 𝐹) → (((𝑎 ∈ V ∧ 𝑎 ≠ 𝐴) ∧ 𝑏 ∈ V) ↔ ((𝐶 ∈ V ∧ 𝐶 ≠ 𝐴) ∧ 𝐹 ∈ V))) |
87 | 81, 86 | anbi12d 743 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 = 𝐶 ∧ 𝑏 = 𝐹) → ((𝑥 = 〈𝑎, 𝑏〉 ∧ ((𝑎 ∈ V ∧ 𝑎 ≠ 𝐴) ∧ 𝑏 ∈ V)) ↔ (𝑥 = 〈𝐶, 𝐹〉 ∧ ((𝐶 ∈ V ∧ 𝐶 ≠ 𝐴) ∧ 𝐹 ∈ V)))) |
88 | 87 | spc2egv 3268 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉) → ((𝑥 = 〈𝐶, 𝐹〉 ∧ ((𝐶 ∈ V ∧ 𝐶 ≠ 𝐴) ∧ 𝐹 ∈ V)) → ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ ((𝑎 ∈ V ∧ 𝑎 ≠ 𝐴) ∧ 𝑏 ∈ V)))) |
89 | 71, 75, 88 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑥 = 〈𝐶, 𝐹〉 ∧ ((𝐶 ∈ V ∧ 𝐶 ≠ 𝐴) ∧ 𝐹 ∈ V)) → ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ ((𝑎 ∈ V ∧ 𝑎 ≠ 𝐴) ∧ 𝑏 ∈ V)))) |
90 | 89 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 〈𝐶, 𝐹〉 ∧ 𝜑) → ((𝑥 = 〈𝐶, 𝐹〉 ∧ ((𝐶 ∈ V ∧ 𝐶 ≠ 𝐴) ∧ 𝐹 ∈ V)) → ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ ((𝑎 ∈ V ∧ 𝑎 ≠ 𝐴) ∧ 𝑏 ∈ V)))) |
91 | 79, 90 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 〈𝐶, 𝐹〉 ∧ 𝜑) → ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ ((𝑎 ∈ V ∧ 𝑎 ≠ 𝐴) ∧ 𝑏 ∈ V))) |
92 | 70, 91 | jaoian 820 |
. . . . . . . . . . 11
⊢ (((𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉) ∧ 𝜑) → ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ ((𝑎 ∈ V ∧ 𝑎 ≠ 𝐴) ∧ 𝑏 ∈ V))) |
93 | 9 | anbi1i 727 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V) ↔ ((𝑎 ∈ V ∧ 𝑎 ≠ 𝐴) ∧ 𝑏 ∈ V)) |
94 | 93 | anbi2i 726 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) ↔ (𝑥 = 〈𝑎, 𝑏〉 ∧ ((𝑎 ∈ V ∧ 𝑎 ≠ 𝐴) ∧ 𝑏 ∈ V))) |
95 | 94 | 2exbii 1765 |
. . . . . . . . . . 11
⊢
(∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) ↔ ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ ((𝑎 ∈ V ∧ 𝑎 ≠ 𝐴) ∧ 𝑏 ∈ V))) |
96 | 92, 95 | sylibr 223 |
. . . . . . . . . 10
⊢ (((𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉) ∧ 𝜑) → ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) |
97 | 49, 96 | jca 553 |
. . . . . . . . 9
⊢ (((𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉) ∧ 𝜑) → (𝑥 ∈ 𝑇 ∧ ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)))) |
98 | 97 | ex 449 |
. . . . . . . 8
⊢ ((𝑥 = 〈𝐵, 𝐸〉 ∨ 𝑥 = 〈𝐶, 𝐹〉) → (𝜑 → (𝑥 ∈ 𝑇 ∧ ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))))) |
99 | 37, 98 | sylbi 206 |
. . . . . . 7
⊢ (𝑥 ∈ {〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉} → (𝜑 → (𝑥 ∈ 𝑇 ∧ ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))))) |
100 | 99 | com12 32 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ {〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉} → (𝑥 ∈ 𝑇 ∧ ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))))) |
101 | 42, 100 | impbid 201 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝑇 ∧ ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) ↔ 𝑥 ∈ {〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉})) |
102 | 4, 101 | syl5bb 271 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑇 ∧ 𝑥 ∈ ((V ∖ {𝐴}) × V)) ↔ 𝑥 ∈ {〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉})) |
103 | 2, 102 | syl5bb 271 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝑇 ∩ ((V ∖ {𝐴}) × V)) ↔ 𝑥 ∈ {〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉})) |
104 | 103 | eqrdv 2608 |
. 2
⊢ (𝜑 → (𝑇 ∩ ((V ∖ {𝐴}) × V)) = {〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}) |
105 | 1, 104 | syl5eq 2656 |
1
⊢ (𝜑 → (𝑇 ↾ (V ∖ {𝐴})) = {〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}) |