Metamath Proof Explorer


Theorem frpoins3xpg

Description: Special case of founded partial induction over a cross product. (Contributed by Scott Fenton, 22-Aug-2024)

Ref Expression
Hypotheses frpoins3xpg.1 ( ( 𝑥𝐴𝑦𝐵 ) → ( ∀ 𝑧𝑤 ( ⟨ 𝑧 , 𝑤 ⟩ ∈ Pred ( 𝑅 , ( 𝐴 × 𝐵 ) , ⟨ 𝑥 , 𝑦 ⟩ ) → 𝜒 ) → 𝜑 ) )
frpoins3xpg.2 ( 𝑥 = 𝑧 → ( 𝜑𝜓 ) )
frpoins3xpg.3 ( 𝑦 = 𝑤 → ( 𝜓𝜒 ) )
frpoins3xpg.4 ( 𝑥 = 𝑋 → ( 𝜑𝜃 ) )
frpoins3xpg.5 ( 𝑦 = 𝑌 → ( 𝜃𝜏 ) )
Assertion frpoins3xpg ( ( ( 𝑅 Fr ( 𝐴 × 𝐵 ) ∧ 𝑅 Po ( 𝐴 × 𝐵 ) ∧ 𝑅 Se ( 𝐴 × 𝐵 ) ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → 𝜏 )

Proof

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 ( 𝐴 × 𝐵 ) ) ∧ ( 𝑋𝐴𝑌𝐵 ) ) → 𝜏 )