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