Step |
Hyp |
Ref |
Expression |
1 |
|
frpoins3xpg.1 |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ∀ 𝑧 ∀ 𝑤 ( 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → 𝜒 ) → 𝜑 ) ) |
2 |
|
frpoins3xpg.2 |
⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ 𝜓 ) ) |
3 |
|
frpoins3xpg.3 |
⊢ ( 𝑦 = 𝑤 → ( 𝜓 ↔ 𝜒 ) ) |
4 |
|
frpoins3xpg.4 |
⊢ ( 𝑥 = 𝑋 → ( 𝜑 ↔ 𝜃 ) ) |
5 |
|
frpoins3xpg.5 |
⊢ ( 𝑦 = 𝑌 → ( 𝜃 ↔ 𝜏 ) ) |
6 |
|
elxp2 |
⊢ ( 𝑝 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑝 = 〈 𝑥 , 𝑦 〉 ) |
7 |
|
nfcv |
⊢ Ⅎ 𝑥 Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 𝑝 ) |
8 |
|
nfsbc1v |
⊢ Ⅎ 𝑥 [ ( 1st ‘ 𝑞 ) / 𝑥 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 |
9 |
7 8
|
nfralw |
⊢ Ⅎ 𝑥 ∀ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 𝑝 ) [ ( 1st ‘ 𝑞 ) / 𝑥 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 |
10 |
|
nfsbc1v |
⊢ Ⅎ 𝑥 [ ( 1st ‘ 𝑝 ) / 𝑥 ] [ ( 2nd ‘ 𝑝 ) / 𝑦 ] 𝜑 |
11 |
9 10
|
nfim |
⊢ Ⅎ 𝑥 ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 𝑝 ) [ ( 1st ‘ 𝑞 ) / 𝑥 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 → [ ( 1st ‘ 𝑝 ) / 𝑥 ] [ ( 2nd ‘ 𝑝 ) / 𝑦 ] 𝜑 ) |
12 |
|
nfv |
⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴 |
13 |
|
nfcv |
⊢ Ⅎ 𝑦 Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 𝑝 ) |
14 |
|
nfcv |
⊢ Ⅎ 𝑦 ( 1st ‘ 𝑞 ) |
15 |
|
nfsbc1v |
⊢ Ⅎ 𝑦 [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 |
16 |
14 15
|
nfsbcw |
⊢ Ⅎ 𝑦 [ ( 1st ‘ 𝑞 ) / 𝑥 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 |
17 |
13 16
|
nfralw |
⊢ Ⅎ 𝑦 ∀ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 𝑝 ) [ ( 1st ‘ 𝑞 ) / 𝑥 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 |
18 |
|
nfcv |
⊢ Ⅎ 𝑦 ( 1st ‘ 𝑝 ) |
19 |
|
nfsbc1v |
⊢ Ⅎ 𝑦 [ ( 2nd ‘ 𝑝 ) / 𝑦 ] 𝜑 |
20 |
18 19
|
nfsbcw |
⊢ Ⅎ 𝑦 [ ( 1st ‘ 𝑝 ) / 𝑥 ] [ ( 2nd ‘ 𝑝 ) / 𝑦 ] 𝜑 |
21 |
17 20
|
nfim |
⊢ Ⅎ 𝑦 ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 𝑝 ) [ ( 1st ‘ 𝑞 ) / 𝑥 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 → [ ( 1st ‘ 𝑝 ) / 𝑥 ] [ ( 2nd ‘ 𝑝 ) / 𝑦 ] 𝜑 ) |
22 |
2
|
sbcbidv |
⊢ ( 𝑥 = 𝑧 → ( [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 ↔ [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜓 ) ) |
23 |
22
|
cbvsbcvw |
⊢ ( [ ( 1st ‘ 𝑞 ) / 𝑥 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 ↔ [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜓 ) |
24 |
3
|
cbvsbcvw |
⊢ ( [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜓 ↔ [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ) |
25 |
24
|
sbcbii |
⊢ ( [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜓 ↔ [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ) |
26 |
23 25
|
bitri |
⊢ ( [ ( 1st ‘ 𝑞 ) / 𝑥 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 ↔ [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ) |
27 |
26
|
ralbii |
⊢ ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) [ ( 1st ‘ 𝑞 ) / 𝑥 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 ↔ ∀ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ) |
28 |
|
impexp |
⊢ ( ( ( 𝑞 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ) → [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ) ↔ ( 𝑞 ∈ ( 𝐴 × 𝐵 ) → ( 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ) ) ) |
29 |
|
elin |
⊢ ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) ∩ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ) ↔ ( 𝑞 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ) ) |
30 |
|
predss |
⊢ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ⊆ ( 𝐴 × 𝐵 ) |
31 |
|
sseqin2 |
⊢ ( Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ⊆ ( 𝐴 × 𝐵 ) ↔ ( ( 𝐴 × 𝐵 ) ∩ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ) = Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ) |
32 |
30 31
|
mpbi |
⊢ ( ( 𝐴 × 𝐵 ) ∩ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ) = Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) |
33 |
32
|
eleq2i |
⊢ ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) ∩ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ) ↔ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ) |
34 |
29 33
|
bitr3i |
⊢ ( ( 𝑞 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ) ↔ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ) |
35 |
34
|
imbi1i |
⊢ ( ( ( 𝑞 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ) → [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ) ↔ ( 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ) ) |
36 |
28 35
|
bitr3i |
⊢ ( ( 𝑞 ∈ ( 𝐴 × 𝐵 ) → ( 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ) ) ↔ ( 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ) ) |
37 |
36
|
albii |
⊢ ( ∀ 𝑞 ( 𝑞 ∈ ( 𝐴 × 𝐵 ) → ( 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ) ) ↔ ∀ 𝑞 ( 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ) ) |
38 |
|
df-ral |
⊢ ( ∀ 𝑞 ∈ ( 𝐴 × 𝐵 ) ( 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ) ↔ ∀ 𝑞 ( 𝑞 ∈ ( 𝐴 × 𝐵 ) → ( 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ) ) ) |
39 |
|
df-ral |
⊢ ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ↔ ∀ 𝑞 ( 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ) ) |
40 |
37 38 39
|
3bitr4ri |
⊢ ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ↔ ∀ 𝑞 ∈ ( 𝐴 × 𝐵 ) ( 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ) ) |
41 |
|
nfv |
⊢ Ⅎ 𝑧 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) |
42 |
|
nfsbc1v |
⊢ Ⅎ 𝑧 [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 |
43 |
41 42
|
nfim |
⊢ Ⅎ 𝑧 ( 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ) |
44 |
|
nfv |
⊢ Ⅎ 𝑤 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) |
45 |
|
nfcv |
⊢ Ⅎ 𝑤 ( 1st ‘ 𝑞 ) |
46 |
|
nfsbc1v |
⊢ Ⅎ 𝑤 [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 |
47 |
45 46
|
nfsbcw |
⊢ Ⅎ 𝑤 [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 |
48 |
44 47
|
nfim |
⊢ Ⅎ 𝑤 ( 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ) |
49 |
|
nfv |
⊢ Ⅎ 𝑞 ( 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → 𝜒 ) |
50 |
|
eleq1 |
⊢ ( 𝑞 = 〈 𝑧 , 𝑤 〉 → ( 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ↔ 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ) ) |
51 |
|
sbcopeq1a |
⊢ ( 𝑞 = 〈 𝑧 , 𝑤 〉 → ( [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ↔ 𝜒 ) ) |
52 |
50 51
|
imbi12d |
⊢ ( 𝑞 = 〈 𝑧 , 𝑤 〉 → ( ( 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ) ↔ ( 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → 𝜒 ) ) ) |
53 |
43 48 49 52
|
ralxpf |
⊢ ( ∀ 𝑞 ∈ ( 𝐴 × 𝐵 ) ( 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ) ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐵 ( 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → 𝜒 ) ) |
54 |
|
r2al |
⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐵 ( 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → 𝜒 ) ↔ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) → ( 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → 𝜒 ) ) ) |
55 |
|
impexp |
⊢ ( ( ( 〈 𝑧 , 𝑤 〉 ∈ ( 𝐴 × 𝐵 ) ∧ 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ) → 𝜒 ) ↔ ( 〈 𝑧 , 𝑤 〉 ∈ ( 𝐴 × 𝐵 ) → ( 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → 𝜒 ) ) ) |
56 |
|
opelxp |
⊢ ( 〈 𝑧 , 𝑤 〉 ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) |
57 |
56
|
imbi1i |
⊢ ( ( 〈 𝑧 , 𝑤 〉 ∈ ( 𝐴 × 𝐵 ) → ( 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → 𝜒 ) ) ↔ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) → ( 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → 𝜒 ) ) ) |
58 |
55 57
|
bitri |
⊢ ( ( ( 〈 𝑧 , 𝑤 〉 ∈ ( 𝐴 × 𝐵 ) ∧ 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ) → 𝜒 ) ↔ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) → ( 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → 𝜒 ) ) ) |
59 |
|
elin |
⊢ ( 〈 𝑧 , 𝑤 〉 ∈ ( ( 𝐴 × 𝐵 ) ∩ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ) ↔ ( 〈 𝑧 , 𝑤 〉 ∈ ( 𝐴 × 𝐵 ) ∧ 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ) ) |
60 |
32
|
eleq2i |
⊢ ( 〈 𝑧 , 𝑤 〉 ∈ ( ( 𝐴 × 𝐵 ) ∩ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ) ↔ 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ) |
61 |
59 60
|
bitr3i |
⊢ ( ( 〈 𝑧 , 𝑤 〉 ∈ ( 𝐴 × 𝐵 ) ∧ 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ) ↔ 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ) |
62 |
61
|
imbi1i |
⊢ ( ( ( 〈 𝑧 , 𝑤 〉 ∈ ( 𝐴 × 𝐵 ) ∧ 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ) → 𝜒 ) ↔ ( 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → 𝜒 ) ) |
63 |
58 62
|
bitr3i |
⊢ ( ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) → ( 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → 𝜒 ) ) ↔ ( 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → 𝜒 ) ) |
64 |
63
|
2albii |
⊢ ( ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) → ( 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → 𝜒 ) ) ↔ ∀ 𝑧 ∀ 𝑤 ( 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → 𝜒 ) ) |
65 |
53 54 64
|
3bitri |
⊢ ( ∀ 𝑞 ∈ ( 𝐴 × 𝐵 ) ( 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → [ ( 1st ‘ 𝑞 ) / 𝑧 ] [ ( 2nd ‘ 𝑞 ) / 𝑤 ] 𝜒 ) ↔ ∀ 𝑧 ∀ 𝑤 ( 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → 𝜒 ) ) |
66 |
27 40 65
|
3bitri |
⊢ ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) [ ( 1st ‘ 𝑞 ) / 𝑥 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 ↔ ∀ 𝑧 ∀ 𝑤 ( 〈 𝑧 , 𝑤 〉 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) → 𝜒 ) ) |
67 |
66 1
|
syl5bi |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) [ ( 1st ‘ 𝑞 ) / 𝑥 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 → 𝜑 ) ) |
68 |
|
predeq3 |
⊢ ( 𝑝 = 〈 𝑥 , 𝑦 〉 → Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 𝑝 ) = Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) ) |
69 |
68
|
raleqdv |
⊢ ( 𝑝 = 〈 𝑥 , 𝑦 〉 → ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 𝑝 ) [ ( 1st ‘ 𝑞 ) / 𝑥 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 ↔ ∀ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) [ ( 1st ‘ 𝑞 ) / 𝑥 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 ) ) |
70 |
|
sbcopeq1a |
⊢ ( 𝑝 = 〈 𝑥 , 𝑦 〉 → ( [ ( 1st ‘ 𝑝 ) / 𝑥 ] [ ( 2nd ‘ 𝑝 ) / 𝑦 ] 𝜑 ↔ 𝜑 ) ) |
71 |
69 70
|
imbi12d |
⊢ ( 𝑝 = 〈 𝑥 , 𝑦 〉 → ( ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 𝑝 ) [ ( 1st ‘ 𝑞 ) / 𝑥 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 → [ ( 1st ‘ 𝑝 ) / 𝑥 ] [ ( 2nd ‘ 𝑝 ) / 𝑦 ] 𝜑 ) ↔ ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 〈 𝑥 , 𝑦 〉 ) [ ( 1st ‘ 𝑞 ) / 𝑥 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 → 𝜑 ) ) ) |
72 |
67 71
|
syl5ibrcom |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑝 = 〈 𝑥 , 𝑦 〉 → ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 𝑝 ) [ ( 1st ‘ 𝑞 ) / 𝑥 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 → [ ( 1st ‘ 𝑝 ) / 𝑥 ] [ ( 2nd ‘ 𝑝 ) / 𝑦 ] 𝜑 ) ) ) |
73 |
72
|
ex |
⊢ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → ( 𝑝 = 〈 𝑥 , 𝑦 〉 → ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 𝑝 ) [ ( 1st ‘ 𝑞 ) / 𝑥 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 → [ ( 1st ‘ 𝑝 ) / 𝑥 ] [ ( 2nd ‘ 𝑝 ) / 𝑦 ] 𝜑 ) ) ) ) |
74 |
12 21 73
|
rexlimd |
⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 ∈ 𝐵 𝑝 = 〈 𝑥 , 𝑦 〉 → ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 𝑝 ) [ ( 1st ‘ 𝑞 ) / 𝑥 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 → [ ( 1st ‘ 𝑝 ) / 𝑥 ] [ ( 2nd ‘ 𝑝 ) / 𝑦 ] 𝜑 ) ) ) |
75 |
11 74
|
rexlimi |
⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑝 = 〈 𝑥 , 𝑦 〉 → ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 𝑝 ) [ ( 1st ‘ 𝑞 ) / 𝑥 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 → [ ( 1st ‘ 𝑝 ) / 𝑥 ] [ ( 2nd ‘ 𝑝 ) / 𝑦 ] 𝜑 ) ) |
76 |
6 75
|
sylbi |
⊢ ( 𝑝 ∈ ( 𝐴 × 𝐵 ) → ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , 𝑝 ) [ ( 1st ‘ 𝑞 ) / 𝑥 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 → [ ( 1st ‘ 𝑝 ) / 𝑥 ] [ ( 2nd ‘ 𝑝 ) / 𝑦 ] 𝜑 ) ) |
77 |
|
fveq2 |
⊢ ( 𝑝 = 𝑞 → ( 1st ‘ 𝑝 ) = ( 1st ‘ 𝑞 ) ) |
78 |
|
fveq2 |
⊢ ( 𝑝 = 𝑞 → ( 2nd ‘ 𝑝 ) = ( 2nd ‘ 𝑞 ) ) |
79 |
78
|
sbceq1d |
⊢ ( 𝑝 = 𝑞 → ( [ ( 2nd ‘ 𝑝 ) / 𝑦 ] 𝜑 ↔ [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 ) ) |
80 |
77 79
|
sbceqbid |
⊢ ( 𝑝 = 𝑞 → ( [ ( 1st ‘ 𝑝 ) / 𝑥 ] [ ( 2nd ‘ 𝑝 ) / 𝑦 ] 𝜑 ↔ [ ( 1st ‘ 𝑞 ) / 𝑥 ] [ ( 2nd ‘ 𝑞 ) / 𝑦 ] 𝜑 ) ) |
81 |
76 80
|
frpoins2g |
⊢ ( ( 𝑅 Fr ( 𝐴 × 𝐵 ) ∧ 𝑅 Po ( 𝐴 × 𝐵 ) ∧ 𝑅 Se ( 𝐴 × 𝐵 ) ) → ∀ 𝑝 ∈ ( 𝐴 × 𝐵 ) [ ( 1st ‘ 𝑝 ) / 𝑥 ] [ ( 2nd ‘ 𝑝 ) / 𝑦 ] 𝜑 ) |
82 |
|
ralxpes |
⊢ ( ∀ 𝑝 ∈ ( 𝐴 × 𝐵 ) [ ( 1st ‘ 𝑝 ) / 𝑥 ] [ ( 2nd ‘ 𝑝 ) / 𝑦 ] 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ) |
83 |
81 82
|
sylib |
⊢ ( ( 𝑅 Fr ( 𝐴 × 𝐵 ) ∧ 𝑅 Po ( 𝐴 × 𝐵 ) ∧ 𝑅 Se ( 𝐴 × 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ) |
84 |
4 5
|
rspc2va |
⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ) → 𝜏 ) |
85 |
83 84
|
sylan2 |
⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑅 Fr ( 𝐴 × 𝐵 ) ∧ 𝑅 Po ( 𝐴 × 𝐵 ) ∧ 𝑅 Se ( 𝐴 × 𝐵 ) ) ) → 𝜏 ) |
86 |
85
|
ancoms |
⊢ ( ( ( 𝑅 Fr ( 𝐴 × 𝐵 ) ∧ 𝑅 Po ( 𝐴 × 𝐵 ) ∧ 𝑅 Se ( 𝐴 × 𝐵 ) ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) → 𝜏 ) |