Metamath Proof Explorer

Theorem frpoins3xpg

Description: Special case of founded partial induction over a Cartesian 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 biimtrid ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ∀ 𝑞 ∈ 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 ( 𝐴 × 𝐵 ) ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) → 𝜏 )