Metamath Proof Explorer


Theorem xpord2pred

Description: Calculate the predecessor class in frxp2 . (Contributed by Scott Fenton, 22-Aug-2024)

Ref Expression
Hypothesis xpord2.1 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ∧ ( ( ( 1st𝑥 ) 𝑅 ( 1st𝑦 ) ∨ ( 1st𝑥 ) = ( 1st𝑦 ) ) ∧ ( ( 2nd𝑥 ) 𝑆 ( 2nd𝑦 ) ∨ ( 2nd𝑥 ) = ( 2nd𝑦 ) ) ∧ 𝑥𝑦 ) ) }
Assertion xpord2pred ( ( 𝑋𝐴𝑌𝐵 ) → Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) ∖ { ⟨ 𝑋 , 𝑌 ⟩ } ) )

Proof

Step Hyp Ref Expression
1 xpord2.1 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ∧ ( ( ( 1st𝑥 ) 𝑅 ( 1st𝑦 ) ∨ ( 1st𝑥 ) = ( 1st𝑦 ) ) ∧ ( ( 2nd𝑥 ) 𝑆 ( 2nd𝑦 ) ∨ ( 2nd𝑥 ) = ( 2nd𝑦 ) ) ∧ 𝑥𝑦 ) ) }
2 opeq1 ( 𝑎 = 𝑋 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑋 , 𝑏 ⟩ )
3 predeq3 ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑋 , 𝑏 ⟩ → Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) = Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑋 , 𝑏 ⟩ ) )
4 2 3 syl ( 𝑎 = 𝑋 → Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) = Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑋 , 𝑏 ⟩ ) )
5 predeq3 ( 𝑎 = 𝑋 → Pred ( 𝑅 , 𝐴 , 𝑎 ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
6 sneq ( 𝑎 = 𝑋 → { 𝑎 } = { 𝑋 } )
7 5 6 uneq12d ( 𝑎 = 𝑋 → ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) = ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) )
8 7 xpeq1d ( 𝑎 = 𝑋 → ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) = ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) )
9 2 sneqd ( 𝑎 = 𝑋 → { ⟨ 𝑎 , 𝑏 ⟩ } = { ⟨ 𝑋 , 𝑏 ⟩ } )
10 8 9 difeq12d ( 𝑎 = 𝑋 → ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) = ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑋 , 𝑏 ⟩ } ) )
11 4 10 eqeq12d ( 𝑎 = 𝑋 → ( Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) = ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ↔ Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑋 , 𝑏 ⟩ ) = ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑋 , 𝑏 ⟩ } ) ) )
12 opeq2 ( 𝑏 = 𝑌 → ⟨ 𝑋 , 𝑏 ⟩ = ⟨ 𝑋 , 𝑌 ⟩ )
13 predeq3 ( ⟨ 𝑋 , 𝑏 ⟩ = ⟨ 𝑋 , 𝑌 ⟩ → Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑋 , 𝑏 ⟩ ) = Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑋 , 𝑌 ⟩ ) )
14 12 13 syl ( 𝑏 = 𝑌 → Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑋 , 𝑏 ⟩ ) = Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑋 , 𝑌 ⟩ ) )
15 predeq3 ( 𝑏 = 𝑌 → Pred ( 𝑆 , 𝐵 , 𝑏 ) = Pred ( 𝑆 , 𝐵 , 𝑌 ) )
16 sneq ( 𝑏 = 𝑌 → { 𝑏 } = { 𝑌 } )
17 15 16 uneq12d ( 𝑏 = 𝑌 → ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) = ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) )
18 17 xpeq2d ( 𝑏 = 𝑌 → ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) = ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) )
19 12 sneqd ( 𝑏 = 𝑌 → { ⟨ 𝑋 , 𝑏 ⟩ } = { ⟨ 𝑋 , 𝑌 ⟩ } )
20 18 19 difeq12d ( 𝑏 = 𝑌 → ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑋 , 𝑏 ⟩ } ) = ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) ∖ { ⟨ 𝑋 , 𝑌 ⟩ } ) )
21 14 20 eqeq12d ( 𝑏 = 𝑌 → ( Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑋 , 𝑏 ⟩ ) = ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑋 , 𝑏 ⟩ } ) ↔ Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) ∖ { ⟨ 𝑋 , 𝑌 ⟩ } ) ) )
22 predel ( 𝑒 ∈ Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) → 𝑒 ∈ ( 𝐴 × 𝐵 ) )
23 22 a1i ( ( 𝑎𝐴𝑏𝐵 ) → ( 𝑒 ∈ Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) → 𝑒 ∈ ( 𝐴 × 𝐵 ) ) )
24 eldifi ( 𝑒 ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) → 𝑒 ∈ ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) )
25 predss Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝐴
26 25 a1i ( 𝑎𝐴 → Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝐴 )
27 snssi ( 𝑎𝐴 → { 𝑎 } ⊆ 𝐴 )
28 26 27 unssd ( 𝑎𝐴 → ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ⊆ 𝐴 )
29 predss Pred ( 𝑆 , 𝐵 , 𝑏 ) ⊆ 𝐵
30 29 a1i ( 𝑏𝐵 → Pred ( 𝑆 , 𝐵 , 𝑏 ) ⊆ 𝐵 )
31 snssi ( 𝑏𝐵 → { 𝑏 } ⊆ 𝐵 )
32 30 31 unssd ( 𝑏𝐵 → ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ⊆ 𝐵 )
33 xpss12 ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ⊆ 𝐴 ∧ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ⊆ 𝐵 ) → ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ⊆ ( 𝐴 × 𝐵 ) )
34 28 32 33 syl2an ( ( 𝑎𝐴𝑏𝐵 ) → ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ⊆ ( 𝐴 × 𝐵 ) )
35 34 sseld ( ( 𝑎𝐴𝑏𝐵 ) → ( 𝑒 ∈ ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) → 𝑒 ∈ ( 𝐴 × 𝐵 ) ) )
36 24 35 syl5 ( ( 𝑎𝐴𝑏𝐵 ) → ( 𝑒 ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) → 𝑒 ∈ ( 𝐴 × 𝐵 ) ) )
37 elxp2 ( 𝑒 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑐𝐴𝑑𝐵 𝑒 = ⟨ 𝑐 , 𝑑 ⟩ )
38 opex 𝑎 , 𝑏 ⟩ ∈ V
39 opex 𝑐 , 𝑑 ⟩ ∈ V
40 39 elpred ( ⟨ 𝑎 , 𝑏 ⟩ ∈ V → ( ⟨ 𝑐 , 𝑑 ⟩ ∈ Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑐 , 𝑑𝑇𝑎 , 𝑏 ⟩ ) ) )
41 38 40 ax-mp ( ⟨ 𝑐 , 𝑑 ⟩ ∈ Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑐 , 𝑑𝑇𝑎 , 𝑏 ⟩ ) )
42 opelxpi ( ( 𝑐𝐴𝑑𝐵 ) → ⟨ 𝑐 , 𝑑 ⟩ ∈ ( 𝐴 × 𝐵 ) )
43 42 adantl ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ⟨ 𝑐 , 𝑑 ⟩ ∈ ( 𝐴 × 𝐵 ) )
44 43 biantrurd ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( ⟨ 𝑐 , 𝑑𝑇𝑎 , 𝑏 ⟩ ↔ ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑐 , 𝑑𝑇𝑎 , 𝑏 ⟩ ) ) )
45 1 xpord2lem ( ⟨ 𝑐 , 𝑑𝑇𝑎 , 𝑏 ⟩ ↔ ( ( 𝑐𝐴𝑑𝐵 ) ∧ ( 𝑎𝐴𝑏𝐵 ) ∧ ( ( 𝑐 𝑅 𝑎𝑐 = 𝑎 ) ∧ ( 𝑑 𝑆 𝑏𝑑 = 𝑏 ) ∧ ( 𝑐𝑎𝑑𝑏 ) ) ) )
46 eldif ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ↔ ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∧ ¬ ⟨ 𝑐 , 𝑑 ⟩ ∈ { ⟨ 𝑎 , 𝑏 ⟩ } ) )
47 opelxp ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ↔ ( 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) )
48 elun ( 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ↔ ( 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∨ 𝑐 ∈ { 𝑎 } ) )
49 vex 𝑐 ∈ V
50 49 elpred ( 𝑎 ∈ V → ( 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ↔ ( 𝑐𝐴𝑐 𝑅 𝑎 ) ) )
51 50 elv ( 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ↔ ( 𝑐𝐴𝑐 𝑅 𝑎 ) )
52 velsn ( 𝑐 ∈ { 𝑎 } ↔ 𝑐 = 𝑎 )
53 51 52 orbi12i ( ( 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∨ 𝑐 ∈ { 𝑎 } ) ↔ ( ( 𝑐𝐴𝑐 𝑅 𝑎 ) ∨ 𝑐 = 𝑎 ) )
54 48 53 bitri ( 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ↔ ( ( 𝑐𝐴𝑐 𝑅 𝑎 ) ∨ 𝑐 = 𝑎 ) )
55 elun ( 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ↔ ( 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∨ 𝑑 ∈ { 𝑏 } ) )
56 vex 𝑑 ∈ V
57 56 elpred ( 𝑏 ∈ V → ( 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ↔ ( 𝑑𝐵𝑑 𝑆 𝑏 ) ) )
58 57 elv ( 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ↔ ( 𝑑𝐵𝑑 𝑆 𝑏 ) )
59 velsn ( 𝑑 ∈ { 𝑏 } ↔ 𝑑 = 𝑏 )
60 58 59 orbi12i ( ( 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∨ 𝑑 ∈ { 𝑏 } ) ↔ ( ( 𝑑𝐵𝑑 𝑆 𝑏 ) ∨ 𝑑 = 𝑏 ) )
61 55 60 bitri ( 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ↔ ( ( 𝑑𝐵𝑑 𝑆 𝑏 ) ∨ 𝑑 = 𝑏 ) )
62 54 61 anbi12i ( ( 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ↔ ( ( ( 𝑐𝐴𝑐 𝑅 𝑎 ) ∨ 𝑐 = 𝑎 ) ∧ ( ( 𝑑𝐵𝑑 𝑆 𝑏 ) ∨ 𝑑 = 𝑏 ) ) )
63 47 62 bitri ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ↔ ( ( ( 𝑐𝐴𝑐 𝑅 𝑎 ) ∨ 𝑐 = 𝑎 ) ∧ ( ( 𝑑𝐵𝑑 𝑆 𝑏 ) ∨ 𝑑 = 𝑏 ) ) )
64 39 elsn ( ⟨ 𝑐 , 𝑑 ⟩ ∈ { ⟨ 𝑎 , 𝑏 ⟩ } ↔ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
65 64 notbii ( ¬ ⟨ 𝑐 , 𝑑 ⟩ ∈ { ⟨ 𝑎 , 𝑏 ⟩ } ↔ ¬ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
66 df-ne ( ⟨ 𝑐 , 𝑑 ⟩ ≠ ⟨ 𝑎 , 𝑏 ⟩ ↔ ¬ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
67 49 56 opthne ( ⟨ 𝑐 , 𝑑 ⟩ ≠ ⟨ 𝑎 , 𝑏 ⟩ ↔ ( 𝑐𝑎𝑑𝑏 ) )
68 65 66 67 3bitr2i ( ¬ ⟨ 𝑐 , 𝑑 ⟩ ∈ { ⟨ 𝑎 , 𝑏 ⟩ } ↔ ( 𝑐𝑎𝑑𝑏 ) )
69 63 68 anbi12i ( ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∧ ¬ ⟨ 𝑐 , 𝑑 ⟩ ∈ { ⟨ 𝑎 , 𝑏 ⟩ } ) ↔ ( ( ( ( 𝑐𝐴𝑐 𝑅 𝑎 ) ∨ 𝑐 = 𝑎 ) ∧ ( ( 𝑑𝐵𝑑 𝑆 𝑏 ) ∨ 𝑑 = 𝑏 ) ) ∧ ( 𝑐𝑎𝑑𝑏 ) ) )
70 46 69 bitri ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ↔ ( ( ( ( 𝑐𝐴𝑐 𝑅 𝑎 ) ∨ 𝑐 = 𝑎 ) ∧ ( ( 𝑑𝐵𝑑 𝑆 𝑏 ) ∨ 𝑑 = 𝑏 ) ) ∧ ( 𝑐𝑎𝑑𝑏 ) ) )
71 simprl ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ) → 𝑐𝐴 )
72 71 biantrurd ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( 𝑐 𝑅 𝑎 ↔ ( 𝑐𝐴𝑐 𝑅 𝑎 ) ) )
73 72 orbi1d ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( ( 𝑐 𝑅 𝑎𝑐 = 𝑎 ) ↔ ( ( 𝑐𝐴𝑐 𝑅 𝑎 ) ∨ 𝑐 = 𝑎 ) ) )
74 simprr ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ) → 𝑑𝐵 )
75 74 biantrurd ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( 𝑑 𝑆 𝑏 ↔ ( 𝑑𝐵𝑑 𝑆 𝑏 ) ) )
76 75 orbi1d ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( ( 𝑑 𝑆 𝑏𝑑 = 𝑏 ) ↔ ( ( 𝑑𝐵𝑑 𝑆 𝑏 ) ∨ 𝑑 = 𝑏 ) ) )
77 73 76 3anbi12d ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( ( ( 𝑐 𝑅 𝑎𝑐 = 𝑎 ) ∧ ( 𝑑 𝑆 𝑏𝑑 = 𝑏 ) ∧ ( 𝑐𝑎𝑑𝑏 ) ) ↔ ( ( ( 𝑐𝐴𝑐 𝑅 𝑎 ) ∨ 𝑐 = 𝑎 ) ∧ ( ( 𝑑𝐵𝑑 𝑆 𝑏 ) ∨ 𝑑 = 𝑏 ) ∧ ( 𝑐𝑎𝑑𝑏 ) ) ) )
78 df-3an ( ( ( ( 𝑐𝐴𝑐 𝑅 𝑎 ) ∨ 𝑐 = 𝑎 ) ∧ ( ( 𝑑𝐵𝑑 𝑆 𝑏 ) ∨ 𝑑 = 𝑏 ) ∧ ( 𝑐𝑎𝑑𝑏 ) ) ↔ ( ( ( ( 𝑐𝐴𝑐 𝑅 𝑎 ) ∨ 𝑐 = 𝑎 ) ∧ ( ( 𝑑𝐵𝑑 𝑆 𝑏 ) ∨ 𝑑 = 𝑏 ) ) ∧ ( 𝑐𝑎𝑑𝑏 ) ) )
79 77 78 bitr2di ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( ( ( ( ( 𝑐𝐴𝑐 𝑅 𝑎 ) ∨ 𝑐 = 𝑎 ) ∧ ( ( 𝑑𝐵𝑑 𝑆 𝑏 ) ∨ 𝑑 = 𝑏 ) ) ∧ ( 𝑐𝑎𝑑𝑏 ) ) ↔ ( ( 𝑐 𝑅 𝑎𝑐 = 𝑎 ) ∧ ( 𝑑 𝑆 𝑏𝑑 = 𝑏 ) ∧ ( 𝑐𝑎𝑑𝑏 ) ) ) )
80 70 79 syl5bb ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ↔ ( ( 𝑐 𝑅 𝑎𝑐 = 𝑎 ) ∧ ( 𝑑 𝑆 𝑏𝑑 = 𝑏 ) ∧ ( 𝑐𝑎𝑑𝑏 ) ) ) )
81 pm3.22 ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( ( 𝑐𝐴𝑑𝐵 ) ∧ ( 𝑎𝐴𝑏𝐵 ) ) )
82 81 biantrurd ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( ( ( 𝑐 𝑅 𝑎𝑐 = 𝑎 ) ∧ ( 𝑑 𝑆 𝑏𝑑 = 𝑏 ) ∧ ( 𝑐𝑎𝑑𝑏 ) ) ↔ ( ( ( 𝑐𝐴𝑑𝐵 ) ∧ ( 𝑎𝐴𝑏𝐵 ) ) ∧ ( ( 𝑐 𝑅 𝑎𝑐 = 𝑎 ) ∧ ( 𝑑 𝑆 𝑏𝑑 = 𝑏 ) ∧ ( 𝑐𝑎𝑑𝑏 ) ) ) ) )
83 df-3an ( ( ( 𝑐𝐴𝑑𝐵 ) ∧ ( 𝑎𝐴𝑏𝐵 ) ∧ ( ( 𝑐 𝑅 𝑎𝑐 = 𝑎 ) ∧ ( 𝑑 𝑆 𝑏𝑑 = 𝑏 ) ∧ ( 𝑐𝑎𝑑𝑏 ) ) ) ↔ ( ( ( 𝑐𝐴𝑑𝐵 ) ∧ ( 𝑎𝐴𝑏𝐵 ) ) ∧ ( ( 𝑐 𝑅 𝑎𝑐 = 𝑎 ) ∧ ( 𝑑 𝑆 𝑏𝑑 = 𝑏 ) ∧ ( 𝑐𝑎𝑑𝑏 ) ) ) )
84 82 83 bitr4di ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( ( ( 𝑐 𝑅 𝑎𝑐 = 𝑎 ) ∧ ( 𝑑 𝑆 𝑏𝑑 = 𝑏 ) ∧ ( 𝑐𝑎𝑑𝑏 ) ) ↔ ( ( 𝑐𝐴𝑑𝐵 ) ∧ ( 𝑎𝐴𝑏𝐵 ) ∧ ( ( 𝑐 𝑅 𝑎𝑐 = 𝑎 ) ∧ ( 𝑑 𝑆 𝑏𝑑 = 𝑏 ) ∧ ( 𝑐𝑎𝑑𝑏 ) ) ) ) )
85 80 84 bitr2d ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( ( ( 𝑐𝐴𝑑𝐵 ) ∧ ( 𝑎𝐴𝑏𝐵 ) ∧ ( ( 𝑐 𝑅 𝑎𝑐 = 𝑎 ) ∧ ( 𝑑 𝑆 𝑏𝑑 = 𝑏 ) ∧ ( 𝑐𝑎𝑑𝑏 ) ) ) ↔ ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) )
86 45 85 syl5bb ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( ⟨ 𝑐 , 𝑑𝑇𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) )
87 44 86 bitr3d ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑐 , 𝑑𝑇𝑎 , 𝑏 ⟩ ) ↔ ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) )
88 41 87 syl5bb ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( ⟨ 𝑐 , 𝑑 ⟩ ∈ Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) )
89 eleq1 ( 𝑒 = ⟨ 𝑐 , 𝑑 ⟩ → ( 𝑒 ∈ Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ⟨ 𝑐 , 𝑑 ⟩ ∈ Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) ) )
90 eleq1 ( 𝑒 = ⟨ 𝑐 , 𝑑 ⟩ → ( 𝑒 ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ↔ ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) )
91 89 90 bibi12d ( 𝑒 = ⟨ 𝑐 , 𝑑 ⟩ → ( ( 𝑒 ∈ Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) ↔ 𝑒 ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) ↔ ( ⟨ 𝑐 , 𝑑 ⟩ ∈ Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) ) )
92 88 91 syl5ibrcom ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( 𝑒 = ⟨ 𝑐 , 𝑑 ⟩ → ( 𝑒 ∈ Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) ↔ 𝑒 ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) ) )
93 92 rexlimdvva ( ( 𝑎𝐴𝑏𝐵 ) → ( ∃ 𝑐𝐴𝑑𝐵 𝑒 = ⟨ 𝑐 , 𝑑 ⟩ → ( 𝑒 ∈ Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) ↔ 𝑒 ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) ) )
94 37 93 syl5bi ( ( 𝑎𝐴𝑏𝐵 ) → ( 𝑒 ∈ ( 𝐴 × 𝐵 ) → ( 𝑒 ∈ Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) ↔ 𝑒 ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) ) )
95 23 36 94 pm5.21ndd ( ( 𝑎𝐴𝑏𝐵 ) → ( 𝑒 ∈ Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) ↔ 𝑒 ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) )
96 95 eqrdv ( ( 𝑎𝐴𝑏𝐵 ) → Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) = ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) )
97 11 21 96 vtocl2ga ( ( 𝑋𝐴𝑌𝐵 ) → Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) ∖ { ⟨ 𝑋 , 𝑌 ⟩ } ) )