| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oteq1 4881 | . . . 4
⊢ (𝑎 = 𝑋 → 〈𝑎, 𝑏, 𝑐〉 = 〈𝑋, 𝑏, 𝑐〉) | 
| 2 |  | predeq3 6324 | . . . 4
⊢
(〈𝑎, 𝑏, 𝑐〉 = 〈𝑋, 𝑏, 𝑐〉 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑋, 𝑏, 𝑐〉)) | 
| 3 | 1, 2 | syl 17 | . . 3
⊢ (𝑎 = 𝑋 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑋, 𝑏, 𝑐〉)) | 
| 4 |  | predeq3 6324 | . . . . . . 7
⊢ (𝑎 = 𝑋 → Pred(𝑅, 𝐴, 𝑎) = Pred(𝑅, 𝐴, 𝑋)) | 
| 5 |  | sneq 4635 | . . . . . . 7
⊢ (𝑎 = 𝑋 → {𝑎} = {𝑋}) | 
| 6 | 4, 5 | uneq12d 4168 | . . . . . 6
⊢ (𝑎 = 𝑋 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) = (Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋})) | 
| 7 | 6 | xpeq1d 5713 | . . . . 5
⊢ (𝑎 = 𝑋 → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}))) | 
| 8 | 7 | xpeq1d 5713 | . . . 4
⊢ (𝑎 = 𝑋 → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}))) | 
| 9 | 1 | sneqd 4637 | . . . 4
⊢ (𝑎 = 𝑋 → {〈𝑎, 𝑏, 𝑐〉} = {〈𝑋, 𝑏, 𝑐〉}) | 
| 10 | 8, 9 | difeq12d 4126 | . . 3
⊢ (𝑎 = 𝑋 → ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑋, 𝑏, 𝑐〉})) | 
| 11 | 3, 10 | eqeq12d 2752 | . 2
⊢ (𝑎 = 𝑋 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑋, 𝑏, 𝑐〉) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑋, 𝑏, 𝑐〉}))) | 
| 12 |  | oteq2 4882 | . . . 4
⊢ (𝑏 = 𝑌 → 〈𝑋, 𝑏, 𝑐〉 = 〈𝑋, 𝑌, 𝑐〉) | 
| 13 |  | predeq3 6324 | . . . 4
⊢
(〈𝑋, 𝑏, 𝑐〉 = 〈𝑋, 𝑌, 𝑐〉 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑋, 𝑏, 𝑐〉) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑋, 𝑌, 𝑐〉)) | 
| 14 | 12, 13 | syl 17 | . . 3
⊢ (𝑏 = 𝑌 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑋, 𝑏, 𝑐〉) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑋, 𝑌, 𝑐〉)) | 
| 15 |  | predeq3 6324 | . . . . . . 7
⊢ (𝑏 = 𝑌 → Pred(𝑆, 𝐵, 𝑏) = Pred(𝑆, 𝐵, 𝑌)) | 
| 16 |  | sneq 4635 | . . . . . . 7
⊢ (𝑏 = 𝑌 → {𝑏} = {𝑌}) | 
| 17 | 15, 16 | uneq12d 4168 | . . . . . 6
⊢ (𝑏 = 𝑌 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) = (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) | 
| 18 | 17 | xpeq2d 5714 | . . . . 5
⊢ (𝑏 = 𝑌 → ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌}))) | 
| 19 | 18 | xpeq1d 5713 | . . . 4
⊢ (𝑏 = 𝑌 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}))) | 
| 20 | 12 | sneqd 4637 | . . . 4
⊢ (𝑏 = 𝑌 → {〈𝑋, 𝑏, 𝑐〉} = {〈𝑋, 𝑌, 𝑐〉}) | 
| 21 | 19, 20 | difeq12d 4126 | . . 3
⊢ (𝑏 = 𝑌 → ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑋, 𝑏, 𝑐〉}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑋, 𝑌, 𝑐〉})) | 
| 22 | 14, 21 | eqeq12d 2752 | . 2
⊢ (𝑏 = 𝑌 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑋, 𝑏, 𝑐〉) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑋, 𝑏, 𝑐〉}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑋, 𝑌, 𝑐〉) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑋, 𝑌, 𝑐〉}))) | 
| 23 |  | oteq3 4883 | . . . 4
⊢ (𝑐 = 𝑍 → 〈𝑋, 𝑌, 𝑐〉 = 〈𝑋, 𝑌, 𝑍〉) | 
| 24 |  | predeq3 6324 | . . . 4
⊢
(〈𝑋, 𝑌, 𝑐〉 = 〈𝑋, 𝑌, 𝑍〉 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑋, 𝑌, 𝑐〉) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑋, 𝑌, 𝑍〉)) | 
| 25 | 23, 24 | syl 17 | . . 3
⊢ (𝑐 = 𝑍 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑋, 𝑌, 𝑐〉) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑋, 𝑌, 𝑍〉)) | 
| 26 |  | predeq3 6324 | . . . . . 6
⊢ (𝑐 = 𝑍 → Pred(𝑇, 𝐶, 𝑐) = Pred(𝑇, 𝐶, 𝑍)) | 
| 27 |  | sneq 4635 | . . . . . 6
⊢ (𝑐 = 𝑍 → {𝑐} = {𝑍}) | 
| 28 | 26, 27 | uneq12d 4168 | . . . . 5
⊢ (𝑐 = 𝑍 → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) = (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) | 
| 29 | 28 | xpeq2d 5714 | . . . 4
⊢ (𝑐 = 𝑍 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍}))) | 
| 30 | 23 | sneqd 4637 | . . . 4
⊢ (𝑐 = 𝑍 → {〈𝑋, 𝑌, 𝑐〉} = {〈𝑋, 𝑌, 𝑍〉}) | 
| 31 | 29, 30 | difeq12d 4126 | . . 3
⊢ (𝑐 = 𝑍 → ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑋, 𝑌, 𝑐〉}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {〈𝑋, 𝑌, 𝑍〉})) | 
| 32 | 25, 31 | eqeq12d 2752 | . 2
⊢ (𝑐 = 𝑍 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑋, 𝑌, 𝑐〉) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑋, 𝑌, 𝑐〉}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑋, 𝑌, 𝑍〉) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {〈𝑋, 𝑌, 𝑍〉}))) | 
| 33 |  | el2xptp 8061 | . . . . . . 7
⊢ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = 〈𝑑, 𝑒, 𝑓〉) | 
| 34 |  | df-3an 1088 | . . . . . . . . . . 11
⊢ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))) | 
| 35 |  | simplrl 776 | . . . . . . . . . . . . . . 15
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → 𝑑 ∈ 𝐴) | 
| 36 |  | simplrr 777 | . . . . . . . . . . . . . . 15
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → 𝑒 ∈ 𝐵) | 
| 37 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → 𝑓 ∈ 𝐶) | 
| 38 | 35, 36, 37 | 3jca 1128 | . . . . . . . . . . . . . 14
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) | 
| 39 |  | simpll 766 | . . . . . . . . . . . . . 14
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) | 
| 40 | 38, 39 | jca 511 | . . . . . . . . . . . . 13
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶))) | 
| 41 | 40 | biantrurd 532 | . . . . . . . . . . . 12
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))) | 
| 42 | 35 | biantrurd 532 | . . . . . . . . . . . . . . 15
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑑𝑅𝑎 ↔ (𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎))) | 
| 43 | 42 | orbi1d 916 | . . . . . . . . . . . . . 14
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ↔ ((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎))) | 
| 44 | 36 | biantrurd 532 | . . . . . . . . . . . . . . 15
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑒𝑆𝑏 ↔ (𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏))) | 
| 45 | 44 | orbi1d 916 | . . . . . . . . . . . . . 14
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ↔ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏))) | 
| 46 | 37 | biantrurd 532 | . . . . . . . . . . . . . . 15
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑓𝑇𝑐 ↔ (𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐))) | 
| 47 | 46 | orbi1d 916 | . . . . . . . . . . . . . 14
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((𝑓𝑇𝑐 ∨ 𝑓 = 𝑐) ↔ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))) | 
| 48 | 43, 45, 47 | 3anbi123d 1437 | . . . . . . . . . . . . 13
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))) | 
| 49 | 48 | anbi1d 631 | . . . . . . . . . . . 12
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))) | 
| 50 | 41, 49 | bitr3d 281 | . . . . . . . . . . 11
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))) | 
| 51 | 34, 50 | bitrid 283 | . . . . . . . . . 10
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))) | 
| 52 |  | breq1 5145 | . . . . . . . . . . . 12
⊢ (𝑞 = 〈𝑑, 𝑒, 𝑓〉 → (𝑞𝑈〈𝑎, 𝑏, 𝑐〉 ↔ 〈𝑑, 𝑒, 𝑓〉𝑈〈𝑎, 𝑏, 𝑐〉)) | 
| 53 |  | xpord3.1 | . . . . . . . . . . . . 13
⊢ 𝑈 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st
‘(1st ‘𝑥))𝑅(1st ‘(1st
‘𝑦)) ∨
(1st ‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑦))) ∧
((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st
‘𝑦)) ∨
(2nd ‘(1st ‘𝑥)) = (2nd ‘(1st
‘𝑦))) ∧
((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))} | 
| 54 | 53 | xpord3lem 8175 | . . . . . . . . . . . 12
⊢
(〈𝑑, 𝑒, 𝑓〉𝑈〈𝑎, 𝑏, 𝑐〉 ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))) | 
| 55 | 52, 54 | bitrdi 287 | . . . . . . . . . . 11
⊢ (𝑞 = 〈𝑑, 𝑒, 𝑓〉 → (𝑞𝑈〈𝑎, 𝑏, 𝑐〉 ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))) | 
| 56 |  | eleq1 2828 | . . . . . . . . . . . 12
⊢ (𝑞 = 〈𝑑, 𝑒, 𝑓〉 → (𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉}) ↔ 〈𝑑, 𝑒, 𝑓〉 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉}))) | 
| 57 |  | eldifsn 4785 | . . . . . . . . . . . . 13
⊢
(〈𝑑, 𝑒, 𝑓〉 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉}) ↔ (〈𝑑, 𝑒, 𝑓〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ 〈𝑑, 𝑒, 𝑓〉 ≠ 〈𝑎, 𝑏, 𝑐〉)) | 
| 58 |  | otelxp 5728 | . . . . . . . . . . . . . . 15
⊢
(〈𝑑, 𝑒, 𝑓〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}))) | 
| 59 |  | elun 4152 | . . . . . . . . . . . . . . . . 17
⊢ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑑 ∈ {𝑎})) | 
| 60 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . 20
⊢ 𝑑 ∈ V | 
| 61 | 60 | elpred 6337 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ V → (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎))) | 
| 62 | 61 | elv 3484 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎)) | 
| 63 |  | velsn 4641 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑑 ∈ {𝑎} ↔ 𝑑 = 𝑎) | 
| 64 | 62, 63 | orbi12i 914 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑑 ∈ {𝑎}) ↔ ((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎)) | 
| 65 | 59, 64 | bitri 275 | . . . . . . . . . . . . . . . 16
⊢ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ ((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎)) | 
| 66 |  | elun 4152 | . . . . . . . . . . . . . . . . 17
⊢ (𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑒 ∈ {𝑏})) | 
| 67 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . 20
⊢ 𝑒 ∈ V | 
| 68 | 67 | elpred 6337 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ∈ V → (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏))) | 
| 69 | 68 | elv 3484 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏)) | 
| 70 |  | velsn 4641 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑒 ∈ {𝑏} ↔ 𝑒 = 𝑏) | 
| 71 | 69, 70 | orbi12i 914 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑒 ∈ {𝑏}) ↔ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) | 
| 72 | 66, 71 | bitri 275 | . . . . . . . . . . . . . . . 16
⊢ (𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) | 
| 73 |  | elun 4152 | . . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ↔ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ∨ 𝑓 ∈ {𝑐})) | 
| 74 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . 20
⊢ 𝑓 ∈ V | 
| 75 | 74 | elpred 6337 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 ∈ V → (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ (𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐))) | 
| 76 | 75 | elv 3484 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ (𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐)) | 
| 77 |  | velsn 4641 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ {𝑐} ↔ 𝑓 = 𝑐) | 
| 78 | 76, 77 | orbi12i 914 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ∨ 𝑓 ∈ {𝑐}) ↔ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) | 
| 79 | 73, 78 | bitri 275 | . . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ↔ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) | 
| 80 | 65, 72, 79 | 3anbi123i 1155 | . . . . . . . . . . . . . . 15
⊢ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))) | 
| 81 | 58, 80 | bitri 275 | . . . . . . . . . . . . . 14
⊢
(〈𝑑, 𝑒, 𝑓〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))) | 
| 82 | 60, 67, 74 | otthne 5490 | . . . . . . . . . . . . . 14
⊢
(〈𝑑, 𝑒, 𝑓〉 ≠ 〈𝑎, 𝑏, 𝑐〉 ↔ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) | 
| 83 | 81, 82 | anbi12i 628 | . . . . . . . . . . . . 13
⊢
((〈𝑑, 𝑒, 𝑓〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ 〈𝑑, 𝑒, 𝑓〉 ≠ 〈𝑎, 𝑏, 𝑐〉) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) | 
| 84 | 57, 83 | bitri 275 | . . . . . . . . . . . 12
⊢
(〈𝑑, 𝑒, 𝑓〉 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉}) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) | 
| 85 | 56, 84 | bitrdi 287 | . . . . . . . . . . 11
⊢ (𝑞 = 〈𝑑, 𝑒, 𝑓〉 → (𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉}) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))) | 
| 86 | 55, 85 | bibi12d 345 | . . . . . . . . . 10
⊢ (𝑞 = 〈𝑑, 𝑒, 𝑓〉 → ((𝑞𝑈〈𝑎, 𝑏, 𝑐〉 ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉})) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))) | 
| 87 | 51, 86 | syl5ibrcom 247 | . . . . . . . . 9
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑞 = 〈𝑑, 𝑒, 𝑓〉 → (𝑞𝑈〈𝑎, 𝑏, 𝑐〉 ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉})))) | 
| 88 | 87 | rexlimdva 3154 | . . . . . . . 8
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) → (∃𝑓 ∈ 𝐶 𝑞 = 〈𝑑, 𝑒, 𝑓〉 → (𝑞𝑈〈𝑎, 𝑏, 𝑐〉 ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉})))) | 
| 89 | 88 | rexlimdvva 3212 | . . . . . . 7
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = 〈𝑑, 𝑒, 𝑓〉 → (𝑞𝑈〈𝑎, 𝑏, 𝑐〉 ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉})))) | 
| 90 | 33, 89 | biimtrid 242 | . . . . . 6
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞𝑈〈𝑎, 𝑏, 𝑐〉 ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉})))) | 
| 91 | 90 | pm5.32d 577 | . . . . 5
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → ((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈〈𝑎, 𝑏, 𝑐〉) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉})))) | 
| 92 |  | otex 5469 | . . . . . 6
⊢
〈𝑎, 𝑏, 𝑐〉 ∈ V | 
| 93 |  | vex 3483 | . . . . . . 7
⊢ 𝑞 ∈ V | 
| 94 | 93 | elpred 6337 | . . . . . 6
⊢
(〈𝑎, 𝑏, 𝑐〉 ∈ V → (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈〈𝑎, 𝑏, 𝑐〉))) | 
| 95 | 92, 94 | ax-mp 5 | . . . . 5
⊢ (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈〈𝑎, 𝑏, 𝑐〉)) | 
| 96 |  | elin 3966 | . . . . 5
⊢ (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉})) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉}))) | 
| 97 | 91, 95, 96 | 3bitr4g 314 | . . . 4
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) ↔ 𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉})))) | 
| 98 | 97 | eqrdv 2734 | . . 3
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) = (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉}))) | 
| 99 |  | predss 6328 | . . . . . . . . . 10
⊢
Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴 | 
| 100 | 99 | a1i 11 | . . . . . . . . 9
⊢ (𝑎 ∈ 𝐴 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴) | 
| 101 |  | snssi 4807 | . . . . . . . . 9
⊢ (𝑎 ∈ 𝐴 → {𝑎} ⊆ 𝐴) | 
| 102 | 100, 101 | unssd 4191 | . . . . . . . 8
⊢ (𝑎 ∈ 𝐴 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴) | 
| 103 | 102 | 3ad2ant1 1133 | . . . . . . 7
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴) | 
| 104 |  | predss 6328 | . . . . . . . . . 10
⊢
Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵 | 
| 105 | 104 | a1i 11 | . . . . . . . . 9
⊢ (𝑏 ∈ 𝐵 → Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵) | 
| 106 |  | snssi 4807 | . . . . . . . . 9
⊢ (𝑏 ∈ 𝐵 → {𝑏} ⊆ 𝐵) | 
| 107 | 105, 106 | unssd 4191 | . . . . . . . 8
⊢ (𝑏 ∈ 𝐵 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) | 
| 108 | 107 | 3ad2ant2 1134 | . . . . . . 7
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) | 
| 109 |  | xpss12 5699 | . . . . . . 7
⊢
(((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴 ∧ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵)) | 
| 110 | 103, 108,
109 | syl2anc 584 | . . . . . 6
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵)) | 
| 111 |  | predss 6328 | . . . . . . . . 9
⊢
Pred(𝑇, 𝐶, 𝑐) ⊆ 𝐶 | 
| 112 | 111 | a1i 11 | . . . . . . . 8
⊢ (𝑐 ∈ 𝐶 → Pred(𝑇, 𝐶, 𝑐) ⊆ 𝐶) | 
| 113 |  | snssi 4807 | . . . . . . . 8
⊢ (𝑐 ∈ 𝐶 → {𝑐} ⊆ 𝐶) | 
| 114 | 112, 113 | unssd 4191 | . . . . . . 7
⊢ (𝑐 ∈ 𝐶 → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶) | 
| 115 | 114 | 3ad2ant3 1135 | . . . . . 6
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶) | 
| 116 |  | xpss12 5699 | . . . . . 6
⊢
((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵) ∧ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶) → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ⊆ ((𝐴 × 𝐵) × 𝐶)) | 
| 117 | 110, 115,
116 | syl2anc 584 | . . . . 5
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ⊆ ((𝐴 × 𝐵) × 𝐶)) | 
| 118 | 117 | ssdifssd 4146 | . . . 4
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉}) ⊆ ((𝐴 × 𝐵) × 𝐶)) | 
| 119 |  | sseqin2 4222 | . . . 4
⊢
(((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉}) ⊆ ((𝐴 × 𝐵) × 𝐶) ↔ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉})) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉})) | 
| 120 | 118, 119 | sylib 218 | . . 3
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉})) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉})) | 
| 121 | 98, 120 | eqtrd 2776 | . 2
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉})) | 
| 122 | 11, 22, 32, 121 | vtocl3ga 3582 | 1
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑋, 𝑌, 𝑍〉) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {〈𝑋, 𝑌, 𝑍〉})) |