Proof of Theorem xpord2ind
Step | Hyp | Ref
| Expression |
1 | | xpord2.1 |
. . . . 5
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd
‘𝑥)𝑆(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))} |
2 | | xpord2ind.1 |
. . . . . 6
⊢ 𝑅 Fr 𝐴 |
3 | 2 | a1i 11 |
. . . . 5
⊢ (⊤
→ 𝑅 Fr 𝐴) |
4 | | xpord2ind.4 |
. . . . . 6
⊢ 𝑆 Fr 𝐵 |
5 | 4 | a1i 11 |
. . . . 5
⊢ (⊤
→ 𝑆 Fr 𝐵) |
6 | 1, 3, 5 | frxp2 33402 |
. . . 4
⊢ (⊤
→ 𝑇 Fr (𝐴 × 𝐵)) |
7 | | xpord2ind.2 |
. . . . . 6
⊢ 𝑅 Po 𝐴 |
8 | 7 | a1i 11 |
. . . . 5
⊢ (⊤
→ 𝑅 Po 𝐴) |
9 | | xpord2ind.5 |
. . . . . 6
⊢ 𝑆 Po 𝐵 |
10 | 9 | a1i 11 |
. . . . 5
⊢ (⊤
→ 𝑆 Po 𝐵) |
11 | 1, 8, 10 | poxp2 33401 |
. . . 4
⊢ (⊤
→ 𝑇 Po (𝐴 × 𝐵)) |
12 | | xpord2ind.3 |
. . . . . 6
⊢ 𝑅 Se 𝐴 |
13 | 12 | a1i 11 |
. . . . 5
⊢ (⊤
→ 𝑅 Se 𝐴) |
14 | | xpord2ind.6 |
. . . . . 6
⊢ 𝑆 Se 𝐵 |
15 | 14 | a1i 11 |
. . . . 5
⊢ (⊤
→ 𝑆 Se 𝐵) |
16 | 1, 13, 15 | sexp2 33404 |
. . . 4
⊢ (⊤
→ 𝑇 Se (𝐴 × 𝐵)) |
17 | 6, 11, 16 | 3jca 1129 |
. . 3
⊢ (⊤
→ (𝑇 Fr (𝐴 × 𝐵) ∧ 𝑇 Po (𝐴 × 𝐵) ∧ 𝑇 Se (𝐴 × 𝐵))) |
18 | 17 | mptru 1549 |
. 2
⊢ (𝑇 Fr (𝐴 × 𝐵) ∧ 𝑇 Po (𝐴 × 𝐵) ∧ 𝑇 Se (𝐴 × 𝐵)) |
19 | 1 | xpord2pred 33403 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) = (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉})) |
20 | 19 | eleq2d 2818 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (〈𝑐, 𝑑〉 ∈ Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) ↔ 〈𝑐, 𝑑〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉}))) |
21 | 20 | imbi1d 345 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((〈𝑐, 𝑑〉 ∈ Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) → 𝜒) ↔ (〈𝑐, 𝑑〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉}) → 𝜒))) |
22 | | eldif 3853 |
. . . . . . . . . 10
⊢
(〈𝑐, 𝑑〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉}) ↔ (〈𝑐, 𝑑〉 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ ¬ 〈𝑐, 𝑑〉 ∈ {〈𝑎, 𝑏〉})) |
23 | | opelxp 5561 |
. . . . . . . . . . 11
⊢
(〈𝑐, 𝑑〉 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}))) |
24 | | opex 5322 |
. . . . . . . . . . . . . 14
⊢
〈𝑐, 𝑑〉 ∈ V |
25 | 24 | elsn 4531 |
. . . . . . . . . . . . 13
⊢
(〈𝑐, 𝑑〉 ∈ {〈𝑎, 𝑏〉} ↔ 〈𝑐, 𝑑〉 = 〈𝑎, 𝑏〉) |
26 | 25 | notbii 323 |
. . . . . . . . . . . 12
⊢ (¬
〈𝑐, 𝑑〉 ∈ {〈𝑎, 𝑏〉} ↔ ¬ 〈𝑐, 𝑑〉 = 〈𝑎, 𝑏〉) |
27 | | df-ne 2935 |
. . . . . . . . . . . 12
⊢
(〈𝑐, 𝑑〉 ≠ 〈𝑎, 𝑏〉 ↔ ¬ 〈𝑐, 𝑑〉 = 〈𝑎, 𝑏〉) |
28 | | vex 3402 |
. . . . . . . . . . . . 13
⊢ 𝑐 ∈ V |
29 | | vex 3402 |
. . . . . . . . . . . . 13
⊢ 𝑑 ∈ V |
30 | 28, 29 | opthne 5340 |
. . . . . . . . . . . 12
⊢
(〈𝑐, 𝑑〉 ≠ 〈𝑎, 𝑏〉 ↔ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) |
31 | 26, 27, 30 | 3bitr2i 302 |
. . . . . . . . . . 11
⊢ (¬
〈𝑐, 𝑑〉 ∈ {〈𝑎, 𝑏〉} ↔ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) |
32 | 23, 31 | anbi12i 630 |
. . . . . . . . . 10
⊢
((〈𝑐, 𝑑〉 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ ¬ 〈𝑐, 𝑑〉 ∈ {〈𝑎, 𝑏〉}) ↔ ((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))) |
33 | 22, 32 | bitri 278 |
. . . . . . . . 9
⊢
(〈𝑐, 𝑑〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉}) ↔ ((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))) |
34 | 33 | imbi1i 353 |
. . . . . . . 8
⊢
((〈𝑐, 𝑑〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉}) → 𝜒) ↔ (((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) → 𝜒)) |
35 | | impexp 454 |
. . . . . . . 8
⊢ ((((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) → 𝜒) ↔ ((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) → ((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒))) |
36 | 34, 35 | bitri 278 |
. . . . . . 7
⊢
((〈𝑐, 𝑑〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {〈𝑎, 𝑏〉}) → 𝜒) ↔ ((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) → ((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒))) |
37 | 21, 36 | bitrdi 290 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((〈𝑐, 𝑑〉 ∈ Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) → 𝜒) ↔ ((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) → ((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒)))) |
38 | 37 | 2albidv 1930 |
. . . . 5
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (∀𝑐∀𝑑(〈𝑐, 𝑑〉 ∈ Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) → 𝜒) ↔ ∀𝑐∀𝑑((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) → ((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒)))) |
39 | | r2al 3113 |
. . . . 5
⊢
(∀𝑐 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) ↔ ∀𝑐∀𝑑((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) → ((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒))) |
40 | 38, 39 | bitr4di 292 |
. . . 4
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (∀𝑐∀𝑑(〈𝑐, 𝑑〉 ∈ Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) → 𝜒) ↔ ∀𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒))) |
41 | | ssun1 4062 |
. . . . . . . . 9
⊢
Pred(𝑅, 𝐴, 𝑎) ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) |
42 | | ssralv 3943 |
. . . . . . . . 9
⊢
(Pred(𝑅, 𝐴, 𝑎) ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒))) |
43 | 41, 42 | ax-mp 5 |
. . . . . . . 8
⊢
(∀𝑐 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒)) |
44 | | ssun1 4062 |
. . . . . . . . . 10
⊢
Pred(𝑆, 𝐵, 𝑏) ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) |
45 | | ssralv 3943 |
. . . . . . . . . 10
⊢
(Pred(𝑆, 𝐵, 𝑏) ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) → (∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒))) |
46 | 44, 45 | ax-mp 5 |
. . . . . . . . 9
⊢
(∀𝑑 ∈
(Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒)) |
47 | 46 | ralimi 3075 |
. . . . . . . 8
⊢
(∀𝑐 ∈
Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒)) |
48 | 43, 47 | syl 17 |
. . . . . . 7
⊢
(∀𝑐 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒)) |
49 | | predpoirr 6157 |
. . . . . . . . . . . . . 14
⊢ (𝑆 Po 𝐵 → ¬ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏)) |
50 | 9, 49 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ¬
𝑏 ∈ Pred(𝑆, 𝐵, 𝑏) |
51 | | eleq1w 2815 |
. . . . . . . . . . . . 13
⊢ (𝑑 = 𝑏 → (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏))) |
52 | 50, 51 | mtbiri 330 |
. . . . . . . . . . . 12
⊢ (𝑑 = 𝑏 → ¬ 𝑑 ∈ Pred(𝑆, 𝐵, 𝑏)) |
53 | 52 | necon2ai 2963 |
. . . . . . . . . . 11
⊢ (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) → 𝑑 ≠ 𝑏) |
54 | 53 | olcd 873 |
. . . . . . . . . 10
⊢ (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) → (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) |
55 | | pm2.27 42 |
. . . . . . . . . 10
⊢ ((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → (((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → 𝜒)) |
56 | 54, 55 | syl 17 |
. . . . . . . . 9
⊢ (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) → (((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → 𝜒)) |
57 | 56 | ralimia 3073 |
. . . . . . . 8
⊢
(∀𝑑 ∈
Pred (𝑆, 𝐵, 𝑏)((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒) |
58 | 57 | ralimi 3075 |
. . . . . . 7
⊢
(∀𝑐 ∈
Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒) |
59 | 48, 58 | syl 17 |
. . . . . 6
⊢
(∀𝑐 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒) |
60 | | ssun2 4063 |
. . . . . . . . . . 11
⊢ {𝑏} ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) |
61 | | ssralv 3943 |
. . . . . . . . . . 11
⊢ ({𝑏} ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) → (∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → ∀𝑑 ∈ {𝑏} ((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒))) |
62 | 60, 61 | ax-mp 5 |
. . . . . . . . . 10
⊢
(∀𝑑 ∈
(Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → ∀𝑑 ∈ {𝑏} ((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒)) |
63 | 62 | ralimi 3075 |
. . . . . . . . 9
⊢
(∀𝑐 ∈
Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ {𝑏} ((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒)) |
64 | 43, 63 | syl 17 |
. . . . . . . 8
⊢
(∀𝑐 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ {𝑏} ((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒)) |
65 | | vex 3402 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
66 | | neeq1 2996 |
. . . . . . . . . . . 12
⊢ (𝑑 = 𝑏 → (𝑑 ≠ 𝑏 ↔ 𝑏 ≠ 𝑏)) |
67 | 66 | orbi2d 915 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝑏 → ((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) ↔ (𝑐 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏))) |
68 | | xpord2ind.8 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑑 → (𝜓 ↔ 𝜒)) |
69 | 68 | equcoms 2032 |
. . . . . . . . . . . 12
⊢ (𝑑 = 𝑏 → (𝜓 ↔ 𝜒)) |
70 | 69 | bicomd 226 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝑏 → (𝜒 ↔ 𝜓)) |
71 | 67, 70 | imbi12d 348 |
. . . . . . . . . 10
⊢ (𝑑 = 𝑏 → (((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) ↔ ((𝑐 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏) → 𝜓))) |
72 | 65, 71 | ralsn 4572 |
. . . . . . . . 9
⊢
(∀𝑑 ∈
{𝑏} ((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) ↔ ((𝑐 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏) → 𝜓)) |
73 | 72 | ralbii 3080 |
. . . . . . . 8
⊢
(∀𝑐 ∈
Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ {𝑏} ((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) ↔ ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑐 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏) → 𝜓)) |
74 | 64, 73 | sylib 221 |
. . . . . . 7
⊢
(∀𝑐 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑐 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏) → 𝜓)) |
75 | | predpoirr 6157 |
. . . . . . . . . . . . 13
⊢ (𝑅 Po 𝐴 → ¬ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎)) |
76 | 7, 75 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ¬
𝑎 ∈ Pred(𝑅, 𝐴, 𝑎) |
77 | | eleq1w 2815 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑎 → (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎))) |
78 | 76, 77 | mtbiri 330 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑎 → ¬ 𝑐 ∈ Pred(𝑅, 𝐴, 𝑎)) |
79 | 78 | necon2ai 2963 |
. . . . . . . . . 10
⊢ (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) → 𝑐 ≠ 𝑎) |
80 | 79 | orcd 872 |
. . . . . . . . 9
⊢ (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) → (𝑐 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏)) |
81 | | pm2.27 42 |
. . . . . . . . 9
⊢ ((𝑐 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏) → (((𝑐 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏) → 𝜓) → 𝜓)) |
82 | 80, 81 | syl 17 |
. . . . . . . 8
⊢ (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) → (((𝑐 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏) → 𝜓) → 𝜓)) |
83 | 82 | ralimia 3073 |
. . . . . . 7
⊢
(∀𝑐 ∈
Pred (𝑅, 𝐴, 𝑎)((𝑐 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏) → 𝜓) → ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓) |
84 | 74, 83 | syl 17 |
. . . . . 6
⊢
(∀𝑐 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓) |
85 | | ssun2 4063 |
. . . . . . . . . 10
⊢ {𝑎} ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) |
86 | | ssralv 3943 |
. . . . . . . . . 10
⊢ ({𝑎} ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → ∀𝑐 ∈ {𝑎}∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒))) |
87 | 85, 86 | ax-mp 5 |
. . . . . . . . 9
⊢
(∀𝑐 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → ∀𝑐 ∈ {𝑎}∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒)) |
88 | 46 | ralimi 3075 |
. . . . . . . . 9
⊢
(∀𝑐 ∈
{𝑎}∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → ∀𝑐 ∈ {𝑎}∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒)) |
89 | 87, 88 | syl 17 |
. . . . . . . 8
⊢
(∀𝑐 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → ∀𝑐 ∈ {𝑎}∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒)) |
90 | | vex 3402 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
91 | | neeq1 2996 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑎 → (𝑐 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎)) |
92 | 91 | orbi1d 916 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑎 → ((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) ↔ (𝑎 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))) |
93 | | xpord2ind.9 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑐 → (𝜃 ↔ 𝜒)) |
94 | 93 | equcoms 2032 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑎 → (𝜃 ↔ 𝜒)) |
95 | 94 | bicomd 226 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑎 → (𝜒 ↔ 𝜃)) |
96 | 92, 95 | imbi12d 348 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑎 → (((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) ↔ ((𝑎 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜃))) |
97 | 96 | ralbidv 3109 |
. . . . . . . . 9
⊢ (𝑐 = 𝑎 → (∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) ↔ ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜃))) |
98 | 90, 97 | ralsn 4572 |
. . . . . . . 8
⊢
(∀𝑐 ∈
{𝑎}∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) ↔ ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜃)) |
99 | 89, 98 | sylib 221 |
. . . . . . 7
⊢
(∀𝑐 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜃)) |
100 | 53 | olcd 873 |
. . . . . . . . 9
⊢ (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) → (𝑎 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) |
101 | | pm2.27 42 |
. . . . . . . . 9
⊢ ((𝑎 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → (((𝑎 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜃) → 𝜃)) |
102 | 100, 101 | syl 17 |
. . . . . . . 8
⊢ (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) → (((𝑎 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜃) → 𝜃)) |
103 | 102 | ralimia 3073 |
. . . . . . 7
⊢
(∀𝑑 ∈
Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜃) → ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜃) |
104 | 99, 103 | syl 17 |
. . . . . 6
⊢
(∀𝑐 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜃) |
105 | 59, 84, 104 | 3jca 1129 |
. . . . 5
⊢
(∀𝑐 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → (∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜃)) |
106 | | xpord2ind.i |
. . . . 5
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜃) → 𝜑)) |
107 | 105, 106 | syl5 34 |
. . . 4
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (∀𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏) → 𝜒) → 𝜑)) |
108 | 40, 107 | sylbid 243 |
. . 3
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (∀𝑐∀𝑑(〈𝑐, 𝑑〉 ∈ Pred(𝑇, (𝐴 × 𝐵), 〈𝑎, 𝑏〉) → 𝜒) → 𝜑)) |
109 | | xpord2ind.7 |
. . 3
⊢ (𝑎 = 𝑐 → (𝜑 ↔ 𝜓)) |
110 | | xpord2ind.11 |
. . 3
⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜏)) |
111 | | xpord2ind.12 |
. . 3
⊢ (𝑏 = 𝑌 → (𝜏 ↔ 𝜂)) |
112 | 108, 109,
68, 110, 111 | frpoins3xpg 33388 |
. 2
⊢ (((𝑇 Fr (𝐴 × 𝐵) ∧ 𝑇 Po (𝐴 × 𝐵) ∧ 𝑇 Se (𝐴 × 𝐵)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) → 𝜂) |
113 | 18, 112 | mpan 690 |
1
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 𝜂) |