| Step | Hyp | Ref
| Expression |
| 1 | | opeq1 4873 |
. . . 4
⊢ (𝑎 = 𝑋 → 〈𝑎, 𝑏〉 = 〈𝑋, 𝑏〉) |
| 2 | | predeq3 6325 |
. . . 4
⊢
(〈𝑎, 𝑏〉 = 〈𝑋, 𝑏〉 → Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) = Pred(𝑇, (𝐴 × 𝐵), 〈𝑋, 𝑏〉)) |
| 3 | 1, 2 | syl 17 |
. . 3
⊢ (𝑎 = 𝑋 → Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) = Pred(𝑇, (𝐴 × 𝐵), 〈𝑋, 𝑏〉)) |
| 4 | | predeq3 6325 |
. . . . . 6
⊢ (𝑎 = 𝑋 → Pred(𝑅, 𝐴, 𝑎) = Pred(𝑅, 𝐴, 𝑋)) |
| 5 | | sneq 4636 |
. . . . . 6
⊢ (𝑎 = 𝑋 → {𝑎} = {𝑋}) |
| 6 | 4, 5 | uneq12d 4169 |
. . . . 5
⊢ (𝑎 = 𝑋 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) = (Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋})) |
| 7 | 6 | xpeq1d 5714 |
. . . 4
⊢ (𝑎 = 𝑋 → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}))) |
| 8 | 1 | sneqd 4638 |
. . . 4
⊢ (𝑎 = 𝑋 → {〈𝑎, 𝑏〉} = {〈𝑋, 𝑏〉}) |
| 9 | 7, 8 | difeq12d 4127 |
. . 3
⊢ (𝑎 = 𝑋 → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉}) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑋, 𝑏〉})) |
| 10 | 3, 9 | eqeq12d 2753 |
. 2
⊢ (𝑎 = 𝑋 → (Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) = (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉}) ↔ Pred(𝑇, (𝐴 × 𝐵), 〈𝑋, 𝑏〉) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑋, 𝑏〉}))) |
| 11 | | opeq2 4874 |
. . . 4
⊢ (𝑏 = 𝑌 → 〈𝑋, 𝑏〉 = 〈𝑋, 𝑌〉) |
| 12 | | predeq3 6325 |
. . . 4
⊢
(〈𝑋, 𝑏〉 = 〈𝑋, 𝑌〉 → Pred(𝑇, (𝐴 × 𝐵), 〈𝑋, 𝑏〉) = Pred(𝑇, (𝐴 × 𝐵), 〈𝑋, 𝑌〉)) |
| 13 | 11, 12 | syl 17 |
. . 3
⊢ (𝑏 = 𝑌 → Pred(𝑇, (𝐴 × 𝐵), 〈𝑋, 𝑏〉) = Pred(𝑇, (𝐴 × 𝐵), 〈𝑋, 𝑌〉)) |
| 14 | | predeq3 6325 |
. . . . . 6
⊢ (𝑏 = 𝑌 → Pred(𝑆, 𝐵, 𝑏) = Pred(𝑆, 𝐵, 𝑌)) |
| 15 | | sneq 4636 |
. . . . . 6
⊢ (𝑏 = 𝑌 → {𝑏} = {𝑌}) |
| 16 | 14, 15 | uneq12d 4169 |
. . . . 5
⊢ (𝑏 = 𝑌 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) = (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) |
| 17 | 16 | xpeq2d 5715 |
. . . 4
⊢ (𝑏 = 𝑌 → ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌}))) |
| 18 | 11 | sneqd 4638 |
. . . 4
⊢ (𝑏 = 𝑌 → {〈𝑋, 𝑏〉} = {〈𝑋, 𝑌〉}) |
| 19 | 17, 18 | difeq12d 4127 |
. . 3
⊢ (𝑏 = 𝑌 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑋, 𝑏〉}) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {〈𝑋, 𝑌〉})) |
| 20 | 13, 19 | eqeq12d 2753 |
. 2
⊢ (𝑏 = 𝑌 → (Pred(𝑇, (𝐴 × 𝐵), 〈𝑋, 𝑏〉) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑋, 𝑏〉}) ↔ Pred(𝑇, (𝐴 × 𝐵), 〈𝑋, 𝑌〉) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {〈𝑋, 𝑌〉}))) |
| 21 | | predel 6342 |
. . . . 5
⊢ (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) → 𝑒 ∈ (𝐴 × 𝐵)) |
| 22 | 21 | a1i 11 |
. . . 4
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) → 𝑒 ∈ (𝐴 × 𝐵))) |
| 23 | | eldifi 4131 |
. . . . 5
⊢ (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉}) → 𝑒 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}))) |
| 24 | | predss 6329 |
. . . . . . . . 9
⊢
Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴 |
| 25 | 24 | a1i 11 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝐴 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴) |
| 26 | | snssi 4808 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝐴 → {𝑎} ⊆ 𝐴) |
| 27 | 25, 26 | unssd 4192 |
. . . . . . 7
⊢ (𝑎 ∈ 𝐴 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴) |
| 28 | | predss 6329 |
. . . . . . . . 9
⊢
Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵 |
| 29 | 28 | a1i 11 |
. . . . . . . 8
⊢ (𝑏 ∈ 𝐵 → Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵) |
| 30 | | snssi 4808 |
. . . . . . . 8
⊢ (𝑏 ∈ 𝐵 → {𝑏} ⊆ 𝐵) |
| 31 | 29, 30 | unssd 4192 |
. . . . . . 7
⊢ (𝑏 ∈ 𝐵 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) |
| 32 | | xpss12 5700 |
. . . . . . 7
⊢
(((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴 ∧ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵)) |
| 33 | 27, 31, 32 | syl2an 596 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵)) |
| 34 | 33 | sseld 3982 |
. . . . 5
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) → 𝑒 ∈ (𝐴 × 𝐵))) |
| 35 | 23, 34 | syl5 34 |
. . . 4
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉}) → 𝑒 ∈ (𝐴 × 𝐵))) |
| 36 | | elxp2 5709 |
. . . . 5
⊢ (𝑒 ∈ (𝐴 × 𝐵) ↔ ∃𝑐 ∈ 𝐴 ∃𝑑 ∈ 𝐵 𝑒 = 〈𝑐, 𝑑〉) |
| 37 | | opex 5469 |
. . . . . . . . 9
⊢
〈𝑎, 𝑏〉 ∈ V |
| 38 | | opex 5469 |
. . . . . . . . . 10
⊢
〈𝑐, 𝑑〉 ∈ V |
| 39 | 38 | elpred 6338 |
. . . . . . . . 9
⊢
(〈𝑎, 𝑏〉 ∈ V →
(〈𝑐, 𝑑〉 ∈ Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) ↔ (〈𝑐, 𝑑〉 ∈ (𝐴 × 𝐵) ∧ 〈𝑐, 𝑑〉𝑇〈𝑎, 𝑏〉))) |
| 40 | 37, 39 | ax-mp 5 |
. . . . . . . 8
⊢
(〈𝑐, 𝑑〉 ∈ Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) ↔ (〈𝑐, 𝑑〉 ∈ (𝐴 × 𝐵) ∧ 〈𝑐, 𝑑〉𝑇〈𝑎, 𝑏〉)) |
| 41 | | opelxpi 5722 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) → 〈𝑐, 𝑑〉 ∈ (𝐴 × 𝐵)) |
| 42 | 41 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → 〈𝑐, 𝑑〉 ∈ (𝐴 × 𝐵)) |
| 43 | 42 | biantrurd 532 |
. . . . . . . . 9
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (〈𝑐, 𝑑〉𝑇〈𝑎, 𝑏〉 ↔ (〈𝑐, 𝑑〉 ∈ (𝐴 × 𝐵) ∧ 〈𝑐, 𝑑〉𝑇〈𝑎, 𝑏〉))) |
| 44 | | xpord2.1 |
. . . . . . . . . . 11
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥)𝑆(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))} |
| 45 | 44 | xpord2lem 8167 |
. . . . . . . . . 10
⊢
(〈𝑐, 𝑑〉𝑇〈𝑎, 𝑏〉 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))) |
| 46 | | eldif 3961 |
. . . . . . . . . . . . 13
⊢
(〈𝑐, 𝑑〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉}) ↔ (〈𝑐, 𝑑〉 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ ¬ 〈𝑐, 𝑑〉 ∈ {〈𝑎, 𝑏〉})) |
| 47 | | opelxp 5721 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑐, 𝑑〉 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}))) |
| 48 | | elun 4153 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑐 ∈ {𝑎})) |
| 49 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑐 ∈ V |
| 50 | 49 | elpred 6338 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ V → (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎))) |
| 51 | 50 | elv 3485 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎)) |
| 52 | | velsn 4642 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 ∈ {𝑎} ↔ 𝑐 = 𝑎) |
| 53 | 51, 52 | orbi12i 915 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑐 ∈ {𝑎}) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎)) |
| 54 | 48, 53 | bitri 275 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎)) |
| 55 | | elun 4153 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑑 ∈ {𝑏})) |
| 56 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑑 ∈ V |
| 57 | 56 | elpred 6338 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ∈ V → (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏))) |
| 58 | 57 | elv 3485 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏)) |
| 59 | | velsn 4642 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑑 ∈ {𝑏} ↔ 𝑑 = 𝑏) |
| 60 | 58, 59 | orbi12i 915 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑑 ∈ {𝑏}) ↔ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) |
| 61 | 55, 60 | bitri 275 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) |
| 62 | 54, 61 | anbi12i 628 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏))) |
| 63 | 47, 62 | bitri 275 |
. . . . . . . . . . . . . 14
⊢
(〈𝑐, 𝑑〉 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏))) |
| 64 | 38 | elsn 4641 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑐, 𝑑〉 ∈ {〈𝑎, 𝑏〉} ↔ 〈𝑐, 𝑑〉 = 〈𝑎, 𝑏〉) |
| 65 | 64 | notbii 320 |
. . . . . . . . . . . . . . 15
⊢ (¬
〈𝑐, 𝑑〉 ∈ {〈𝑎, 𝑏〉} ↔ ¬ 〈𝑐, 𝑑〉 = 〈𝑎, 𝑏〉) |
| 66 | | df-ne 2941 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑐, 𝑑〉 ≠ 〈𝑎, 𝑏〉 ↔ ¬ 〈𝑐, 𝑑〉 = 〈𝑎, 𝑏〉) |
| 67 | 49, 56 | opthne 5487 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑐, 𝑑〉 ≠ 〈𝑎, 𝑏〉 ↔ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) |
| 68 | 65, 66, 67 | 3bitr2i 299 |
. . . . . . . . . . . . . 14
⊢ (¬
〈𝑐, 𝑑〉 ∈ {〈𝑎, 𝑏〉} ↔ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) |
| 69 | 63, 68 | anbi12i 628 |
. . . . . . . . . . . . 13
⊢
((〈𝑐, 𝑑〉 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ ¬ 〈𝑐, 𝑑〉 ∈ {〈𝑎, 𝑏〉}) ↔ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))) |
| 70 | 46, 69 | bitri 275 |
. . . . . . . . . . . 12
⊢
(〈𝑐, 𝑑〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉}) ↔ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))) |
| 71 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → 𝑐 ∈ 𝐴) |
| 72 | 71 | biantrurd 532 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (𝑐𝑅𝑎 ↔ (𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎))) |
| 73 | 72 | orbi1d 917 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎))) |
| 74 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → 𝑑 ∈ 𝐵) |
| 75 | 74 | biantrurd 532 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (𝑑𝑆𝑏 ↔ (𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏))) |
| 76 | 75 | orbi1d 917 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ↔ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏))) |
| 77 | 73, 76 | 3anbi12d 1439 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))) |
| 78 | | df-3an 1089 |
. . . . . . . . . . . . 13
⊢ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))) |
| 79 | 77, 78 | bitr2di 288 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))) |
| 80 | 70, 79 | bitrid 283 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (〈𝑐, 𝑑〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉}) ↔ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))) |
| 81 | | pm3.22 459 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵))) |
| 82 | 81 | biantrurd 532 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))) |
| 83 | | df-3an 1089 |
. . . . . . . . . . . 12
⊢ (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))) |
| 84 | 82, 83 | bitr4di 289 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))) |
| 85 | 80, 84 | bitr2d 280 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))) ↔ 〈𝑐, 𝑑〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉}))) |
| 86 | 45, 85 | bitrid 283 |
. . . . . . . . 9
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (〈𝑐, 𝑑〉𝑇〈𝑎, 𝑏〉 ↔ 〈𝑐, 𝑑〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉}))) |
| 87 | 43, 86 | bitr3d 281 |
. . . . . . . 8
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((〈𝑐, 𝑑〉 ∈ (𝐴 × 𝐵) ∧ 〈𝑐, 𝑑〉𝑇〈𝑎, 𝑏〉) ↔ 〈𝑐, 𝑑〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉}))) |
| 88 | 40, 87 | bitrid 283 |
. . . . . . 7
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (〈𝑐, 𝑑〉 ∈ Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) ↔ 〈𝑐, 𝑑〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉}))) |
| 89 | | eleq1 2829 |
. . . . . . . 8
⊢ (𝑒 = 〈𝑐, 𝑑〉 → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) ↔ 〈𝑐, 𝑑〉 ∈ Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉))) |
| 90 | | eleq1 2829 |
. . . . . . . 8
⊢ (𝑒 = 〈𝑐, 𝑑〉 → (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉}) ↔ 〈𝑐, 𝑑〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉}))) |
| 91 | 89, 90 | bibi12d 345 |
. . . . . . 7
⊢ (𝑒 = 〈𝑐, 𝑑〉 → ((𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉})) ↔ (〈𝑐, 𝑑〉 ∈ Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) ↔ 〈𝑐, 𝑑〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉})))) |
| 92 | 88, 91 | syl5ibrcom 247 |
. . . . . 6
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (𝑒 = 〈𝑐, 𝑑〉 → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉})))) |
| 93 | 92 | rexlimdvva 3213 |
. . . . 5
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (∃𝑐 ∈ 𝐴 ∃𝑑 ∈ 𝐵 𝑒 = 〈𝑐, 𝑑〉 → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉})))) |
| 94 | 36, 93 | biimtrid 242 |
. . . 4
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ (𝐴 × 𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉})))) |
| 95 | 22, 35, 94 | pm5.21ndd 379 |
. . 3
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉}))) |
| 96 | 95 | eqrdv 2735 |
. 2
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) = (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉})) |
| 97 | 10, 20, 96 | vtocl2ga 3578 |
1
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → Pred(𝑇, (𝐴 × 𝐵), 〈𝑋, 𝑌〉) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {〈𝑋, 𝑌〉})) |