Step | Hyp | Ref
| Expression |
1 | | opeq1 4805 |
. . . . 5
⊢ (𝑎 = 𝑋 → 〈𝑎, 𝑏〉 = 〈𝑋, 𝑏〉) |
2 | 1 | opeq1d 4811 |
. . . 4
⊢ (𝑎 = 𝑋 → 〈〈𝑎, 𝑏〉, 𝑐〉 = 〈〈𝑋, 𝑏〉, 𝑐〉) |
3 | | predeq3 6210 |
. . . 4
⊢
(〈〈𝑎,
𝑏〉, 𝑐〉 = 〈〈𝑋, 𝑏〉, 𝑐〉 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑎, 𝑏〉, 𝑐〉) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑋, 𝑏〉, 𝑐〉)) |
4 | 2, 3 | syl 17 |
. . 3
⊢ (𝑎 = 𝑋 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑎, 𝑏〉, 𝑐〉) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑋, 𝑏〉, 𝑐〉)) |
5 | | predeq3 6210 |
. . . . . . 7
⊢ (𝑎 = 𝑋 → Pred(𝑅, 𝐴, 𝑎) = Pred(𝑅, 𝐴, 𝑋)) |
6 | | sneq 4572 |
. . . . . . 7
⊢ (𝑎 = 𝑋 → {𝑎} = {𝑋}) |
7 | 5, 6 | uneq12d 4099 |
. . . . . 6
⊢ (𝑎 = 𝑋 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) = (Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋})) |
8 | 7 | xpeq1d 5619 |
. . . . 5
⊢ (𝑎 = 𝑋 → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}))) |
9 | 8 | xpeq1d 5619 |
. . . 4
⊢ (𝑎 = 𝑋 → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}))) |
10 | 2 | sneqd 4574 |
. . . 4
⊢ (𝑎 = 𝑋 → {〈〈𝑎, 𝑏〉, 𝑐〉} = {〈〈𝑋, 𝑏〉, 𝑐〉}) |
11 | 9, 10 | difeq12d 4059 |
. . 3
⊢ (𝑎 = 𝑋 → ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑋, 𝑏〉, 𝑐〉})) |
12 | 4, 11 | eqeq12d 2755 |
. 2
⊢ (𝑎 = 𝑋 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑎, 𝑏〉, 𝑐〉) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑋, 𝑏〉, 𝑐〉) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑋, 𝑏〉, 𝑐〉}))) |
13 | | opeq2 4806 |
. . . . 5
⊢ (𝑏 = 𝑌 → 〈𝑋, 𝑏〉 = 〈𝑋, 𝑌〉) |
14 | 13 | opeq1d 4811 |
. . . 4
⊢ (𝑏 = 𝑌 → 〈〈𝑋, 𝑏〉, 𝑐〉 = 〈〈𝑋, 𝑌〉, 𝑐〉) |
15 | | predeq3 6210 |
. . . 4
⊢
(〈〈𝑋,
𝑏〉, 𝑐〉 = 〈〈𝑋, 𝑌〉, 𝑐〉 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑋, 𝑏〉, 𝑐〉) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑋, 𝑌〉, 𝑐〉)) |
16 | 14, 15 | syl 17 |
. . 3
⊢ (𝑏 = 𝑌 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑋, 𝑏〉, 𝑐〉) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑋, 𝑌〉, 𝑐〉)) |
17 | | predeq3 6210 |
. . . . . . 7
⊢ (𝑏 = 𝑌 → Pred(𝑆, 𝐵, 𝑏) = Pred(𝑆, 𝐵, 𝑌)) |
18 | | sneq 4572 |
. . . . . . 7
⊢ (𝑏 = 𝑌 → {𝑏} = {𝑌}) |
19 | 17, 18 | uneq12d 4099 |
. . . . . 6
⊢ (𝑏 = 𝑌 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) = (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) |
20 | 19 | xpeq2d 5620 |
. . . . 5
⊢ (𝑏 = 𝑌 → ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌}))) |
21 | 20 | xpeq1d 5619 |
. . . 4
⊢ (𝑏 = 𝑌 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}))) |
22 | 14 | sneqd 4574 |
. . . 4
⊢ (𝑏 = 𝑌 → {〈〈𝑋, 𝑏〉, 𝑐〉} = {〈〈𝑋, 𝑌〉, 𝑐〉}) |
23 | 21, 22 | difeq12d 4059 |
. . 3
⊢ (𝑏 = 𝑌 → ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑋, 𝑏〉, 𝑐〉}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑋, 𝑌〉, 𝑐〉})) |
24 | 16, 23 | eqeq12d 2755 |
. 2
⊢ (𝑏 = 𝑌 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑋, 𝑏〉, 𝑐〉) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑋, 𝑏〉, 𝑐〉}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑋, 𝑌〉, 𝑐〉) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑋, 𝑌〉, 𝑐〉}))) |
25 | | opeq2 4806 |
. . . 4
⊢ (𝑐 = 𝑍 → 〈〈𝑋, 𝑌〉, 𝑐〉 = 〈〈𝑋, 𝑌〉, 𝑍〉) |
26 | | predeq3 6210 |
. . . 4
⊢
(〈〈𝑋,
𝑌〉, 𝑐〉 = 〈〈𝑋, 𝑌〉, 𝑍〉 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑋, 𝑌〉, 𝑐〉) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑋, 𝑌〉, 𝑍〉)) |
27 | 25, 26 | syl 17 |
. . 3
⊢ (𝑐 = 𝑍 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑋, 𝑌〉, 𝑐〉) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑋, 𝑌〉, 𝑍〉)) |
28 | | predeq3 6210 |
. . . . . 6
⊢ (𝑐 = 𝑍 → Pred(𝑇, 𝐶, 𝑐) = Pred(𝑇, 𝐶, 𝑍)) |
29 | | sneq 4572 |
. . . . . 6
⊢ (𝑐 = 𝑍 → {𝑐} = {𝑍}) |
30 | 28, 29 | uneq12d 4099 |
. . . . 5
⊢ (𝑐 = 𝑍 → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) = (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) |
31 | 30 | xpeq2d 5620 |
. . . 4
⊢ (𝑐 = 𝑍 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍}))) |
32 | 25 | sneqd 4574 |
. . . 4
⊢ (𝑐 = 𝑍 → {〈〈𝑋, 𝑌〉, 𝑐〉} = {〈〈𝑋, 𝑌〉, 𝑍〉}) |
33 | 31, 32 | difeq12d 4059 |
. . 3
⊢ (𝑐 = 𝑍 → ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑋, 𝑌〉, 𝑐〉}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {〈〈𝑋, 𝑌〉, 𝑍〉})) |
34 | 27, 33 | eqeq12d 2755 |
. 2
⊢ (𝑐 = 𝑍 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑋, 𝑌〉, 𝑐〉) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑋, 𝑌〉, 𝑐〉}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑋, 𝑌〉, 𝑍〉) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {〈〈𝑋, 𝑌〉, 𝑍〉}))) |
35 | | elxpxp 33692 |
. . . . . . 7
⊢ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = 〈〈𝑑, 𝑒〉, 𝑓〉) |
36 | | df-3an 1088 |
. . . . . . . . . . 11
⊢ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵) ∧ 𝑓 ∈ 𝐶)) |
37 | | df-3an 1088 |
. . . . . . . . . . . . 13
⊢ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))) |
38 | | eldif 3898 |
. . . . . . . . . . . . . . . 16
⊢
(〈〈𝑑,
𝑒〉, 𝑓〉 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉}) ↔ (〈〈𝑑, 𝑒〉, 𝑓〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ¬ 〈〈𝑑, 𝑒〉, 𝑓〉 ∈ {〈〈𝑎, 𝑏〉, 𝑐〉})) |
39 | | opelxp 5626 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈〈𝑑,
𝑒〉, 𝑓〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (〈𝑑, 𝑒〉 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}))) |
40 | | opelxp 5626 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑑, 𝑒〉 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}))) |
41 | | elun 4084 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑑 ∈ {𝑎})) |
42 | | vex 3437 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑑 ∈ V |
43 | 42 | elpred 6223 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 ∈ V → (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎))) |
44 | 43 | elv 3439 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎)) |
45 | | velsn 4578 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑑 ∈ {𝑎} ↔ 𝑑 = 𝑎) |
46 | 44, 45 | orbi12i 912 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑑 ∈ {𝑎}) ↔ ((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎)) |
47 | 41, 46 | bitri 274 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ ((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎)) |
48 | | elun 4084 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑒 ∈ {𝑏})) |
49 | | vex 3437 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑒 ∈ V |
50 | 49 | elpred 6223 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 ∈ V → (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏))) |
51 | 50 | elv 3439 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏)) |
52 | | velsn 4578 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑒 ∈ {𝑏} ↔ 𝑒 = 𝑏) |
53 | 51, 52 | orbi12i 912 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑒 ∈ {𝑏}) ↔ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) |
54 | 48, 53 | bitri 274 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) |
55 | 47, 54 | anbi12i 627 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏))) |
56 | 40, 55 | bitri 274 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑑, 𝑒〉 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏))) |
57 | | elun 4084 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ↔ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ∨ 𝑓 ∈ {𝑐})) |
58 | | vex 3437 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑓 ∈ V |
59 | 58 | elpred 6223 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑐 ∈ V → (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ (𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐))) |
60 | 59 | elv 3439 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ (𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐)) |
61 | | velsn 4578 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ {𝑐} ↔ 𝑓 = 𝑐) |
62 | 60, 61 | orbi12i 912 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ∨ 𝑓 ∈ {𝑐}) ↔ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) |
63 | 57, 62 | bitri 274 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ↔ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) |
64 | 56, 63 | anbi12i 627 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈𝑑, 𝑒〉 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))) |
65 | 39, 64 | bitri 274 |
. . . . . . . . . . . . . . . . 17
⊢
(〈〈𝑑,
𝑒〉, 𝑓〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))) |
66 | | df-ne 2945 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈〈𝑑,
𝑒〉, 𝑓〉 ≠ 〈〈𝑎, 𝑏〉, 𝑐〉 ↔ ¬ 〈〈𝑑, 𝑒〉, 𝑓〉 = 〈〈𝑎, 𝑏〉, 𝑐〉) |
67 | 42, 49, 58 | otthne 33691 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈〈𝑑,
𝑒〉, 𝑓〉 ≠ 〈〈𝑎, 𝑏〉, 𝑐〉 ↔ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) |
68 | 66, 67 | bitr3i 276 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
〈〈𝑑, 𝑒〉, 𝑓〉 = 〈〈𝑎, 𝑏〉, 𝑐〉 ↔ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) |
69 | | opex 5380 |
. . . . . . . . . . . . . . . . . . 19
⊢
〈〈𝑑, 𝑒〉, 𝑓〉 ∈ V |
70 | 69 | elsn 4577 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈〈𝑑,
𝑒〉, 𝑓〉 ∈ {〈〈𝑎, 𝑏〉, 𝑐〉} ↔ 〈〈𝑑, 𝑒〉, 𝑓〉 = 〈〈𝑎, 𝑏〉, 𝑐〉) |
71 | 68, 70 | xchnxbir 333 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
〈〈𝑑, 𝑒〉, 𝑓〉 ∈ {〈〈𝑎, 𝑏〉, 𝑐〉} ↔ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) |
72 | 65, 71 | anbi12i 627 |
. . . . . . . . . . . . . . . 16
⊢
((〈〈𝑑,
𝑒〉, 𝑓〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ¬ 〈〈𝑑, 𝑒〉, 𝑓〉 ∈ {〈〈𝑎, 𝑏〉, 𝑐〉}) ↔ (((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) |
73 | 38, 72 | bitri 274 |
. . . . . . . . . . . . . . 15
⊢
(〈〈𝑑,
𝑒〉, 𝑓〉 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉}) ↔ (((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) |
74 | | simpr1 1193 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) → 𝑑 ∈ 𝐴) |
75 | 74 | biantrurd 533 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) → (𝑑𝑅𝑎 ↔ (𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎))) |
76 | 75 | orbi1d 914 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) → ((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ↔ ((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎))) |
77 | | simpr2 1194 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) → 𝑒 ∈ 𝐵) |
78 | 77 | biantrurd 533 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) → (𝑒𝑆𝑏 ↔ (𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏))) |
79 | 78 | orbi1d 914 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) → ((𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ↔ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏))) |
80 | | simpr3 1195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) → 𝑓 ∈ 𝐶) |
81 | 80 | biantrurd 533 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) → (𝑓𝑇𝑐 ↔ (𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐))) |
82 | 81 | orbi1d 914 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) → ((𝑓𝑇𝑐 ∨ 𝑓 = 𝑐) ↔ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))) |
83 | 76, 79, 82 | 3anbi123d 1435 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) → (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))) |
84 | | df-3an 1088 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))) |
85 | 83, 84 | bitrdi 287 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) → (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))) |
86 | 85 | anbi1d 630 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) → ((((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) ↔ (((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))) |
87 | 73, 86 | bitr4id 290 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) → (〈〈𝑑, 𝑒〉, 𝑓〉 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉}) ↔ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))) |
88 | | pm3.22 460 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) → ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶))) |
89 | 88 | biantrurd 533 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) → ((((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))) |
90 | 87, 89 | bitr2d 279 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) → ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) ↔ 〈〈𝑑, 𝑒〉, 𝑓〉 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉}))) |
91 | 37, 90 | syl5bb 283 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) → (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) ↔ 〈〈𝑑, 𝑒〉, 𝑓〉 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉}))) |
92 | | breq1 5078 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = 〈〈𝑑, 𝑒〉, 𝑓〉 → (𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉 ↔ 〈〈𝑑, 𝑒〉, 𝑓〉𝑈〈〈𝑎, 𝑏〉, 𝑐〉)) |
93 | | xpord3.1 |
. . . . . . . . . . . . . . 15
⊢ 𝑈 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st
‘(1st ‘𝑥))𝑅(1st ‘(1st
‘𝑦)) ∨
(1st ‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑦))) ∧
((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st
‘𝑦)) ∨
(2nd ‘(1st ‘𝑥)) = (2nd ‘(1st
‘𝑦))) ∧
((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))} |
94 | 93 | xpord3lem 33804 |
. . . . . . . . . . . . . 14
⊢
(〈〈𝑑,
𝑒〉, 𝑓〉𝑈〈〈𝑎, 𝑏〉, 𝑐〉 ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))) |
95 | 92, 94 | bitrdi 287 |
. . . . . . . . . . . . 13
⊢ (𝑞 = 〈〈𝑑, 𝑒〉, 𝑓〉 → (𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉 ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))) |
96 | | eleq1 2827 |
. . . . . . . . . . . . 13
⊢ (𝑞 = 〈〈𝑑, 𝑒〉, 𝑓〉 → (𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉}) ↔ 〈〈𝑑, 𝑒〉, 𝑓〉 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉}))) |
97 | 95, 96 | bibi12d 346 |
. . . . . . . . . . . 12
⊢ (𝑞 = 〈〈𝑑, 𝑒〉, 𝑓〉 → ((𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉 ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉})) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) ↔ 〈〈𝑑, 𝑒〉, 𝑓〉 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉})))) |
98 | 91, 97 | syl5ibrcom 246 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) → (𝑞 = 〈〈𝑑, 𝑒〉, 𝑓〉 → (𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉 ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉})))) |
99 | 36, 98 | sylan2br 595 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵) ∧ 𝑓 ∈ 𝐶)) → (𝑞 = 〈〈𝑑, 𝑒〉, 𝑓〉 → (𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉 ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉})))) |
100 | 99 | anassrs 468 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑞 = 〈〈𝑑, 𝑒〉, 𝑓〉 → (𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉 ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉})))) |
101 | 100 | rexlimdva 3214 |
. . . . . . . 8
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) → (∃𝑓 ∈ 𝐶 𝑞 = 〈〈𝑑, 𝑒〉, 𝑓〉 → (𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉 ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉})))) |
102 | 101 | rexlimdvva 3224 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = 〈〈𝑑, 𝑒〉, 𝑓〉 → (𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉 ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉})))) |
103 | 35, 102 | syl5bi 241 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉 ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉})))) |
104 | 103 | pm5.32d 577 |
. . . . 5
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → ((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉})))) |
105 | | opex 5380 |
. . . . . 6
⊢
〈〈𝑎, 𝑏〉, 𝑐〉 ∈ V |
106 | | vex 3437 |
. . . . . . 7
⊢ 𝑞 ∈ V |
107 | 106 | elpred 6223 |
. . . . . 6
⊢
(〈〈𝑎,
𝑏〉, 𝑐〉 ∈ V → (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑎, 𝑏〉, 𝑐〉) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉))) |
108 | 105, 107 | ax-mp 5 |
. . . . 5
⊢ (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑎, 𝑏〉, 𝑐〉) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈〈〈𝑎, 𝑏〉, 𝑐〉)) |
109 | | elin 3904 |
. . . . 5
⊢ (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉})) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉}))) |
110 | 104, 108,
109 | 3bitr4g 314 |
. . . 4
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑎, 𝑏〉, 𝑐〉) ↔ 𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉})))) |
111 | 110 | eqrdv 2737 |
. . 3
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑎, 𝑏〉, 𝑐〉) = (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉}))) |
112 | | predss 6214 |
. . . . . . . . . 10
⊢
Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴 |
113 | 112 | a1i 11 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝐴 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴) |
114 | | snssi 4742 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝐴 → {𝑎} ⊆ 𝐴) |
115 | 113, 114 | unssd 4121 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝐴 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴) |
116 | 115 | 3ad2ant1 1132 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴) |
117 | | predss 6214 |
. . . . . . . . . 10
⊢
Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵 |
118 | 117 | a1i 11 |
. . . . . . . . 9
⊢ (𝑏 ∈ 𝐵 → Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵) |
119 | | snssi 4742 |
. . . . . . . . 9
⊢ (𝑏 ∈ 𝐵 → {𝑏} ⊆ 𝐵) |
120 | 118, 119 | unssd 4121 |
. . . . . . . 8
⊢ (𝑏 ∈ 𝐵 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) |
121 | 120 | 3ad2ant2 1133 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) |
122 | | xpss12 5605 |
. . . . . . 7
⊢
(((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴 ∧ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵)) |
123 | 116, 121,
122 | syl2anc 584 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵)) |
124 | | predss 6214 |
. . . . . . . . 9
⊢
Pred(𝑇, 𝐶, 𝑐) ⊆ 𝐶 |
125 | 124 | a1i 11 |
. . . . . . . 8
⊢ (𝑐 ∈ 𝐶 → Pred(𝑇, 𝐶, 𝑐) ⊆ 𝐶) |
126 | | snssi 4742 |
. . . . . . . 8
⊢ (𝑐 ∈ 𝐶 → {𝑐} ⊆ 𝐶) |
127 | 125, 126 | unssd 4121 |
. . . . . . 7
⊢ (𝑐 ∈ 𝐶 → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶) |
128 | 127 | 3ad2ant3 1134 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶) |
129 | | xpss12 5605 |
. . . . . 6
⊢
((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵) ∧ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶) → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ⊆ ((𝐴 × 𝐵) × 𝐶)) |
130 | 123, 128,
129 | syl2anc 584 |
. . . . 5
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ⊆ ((𝐴 × 𝐵) × 𝐶)) |
131 | 130 | ssdifssd 4078 |
. . . 4
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉}) ⊆ ((𝐴 × 𝐵) × 𝐶)) |
132 | | sseqin2 4150 |
. . . 4
⊢
(((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉}) ⊆ ((𝐴 × 𝐵) × 𝐶) ↔ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉})) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉})) |
133 | 131, 132 | sylib 217 |
. . 3
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉})) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉})) |
134 | 111, 133 | eqtrd 2779 |
. 2
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑎, 𝑏〉, 𝑐〉) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈〈𝑎, 𝑏〉, 𝑐〉})) |
135 | 12, 24, 34, 134 | vtocl3ga 3518 |
1
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈〈𝑋, 𝑌〉, 𝑍〉) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {〈〈𝑋, 𝑌〉, 𝑍〉})) |