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 bitrid ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) → ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ↔ ( ( 𝑐 𝑅 𝑎 ∨ 𝑐 = 𝑎 ) ∧ ( 𝑑 𝑆 𝑏 ∨ 𝑑 = 𝑏 ) ∧ ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) ) ) )
81 pm3.22 ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) → ( ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) )
82 81 biantrurd ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) → ( ( ( 𝑐 𝑅 𝑎 ∨ 𝑐 = 𝑎 ) ∧ ( 𝑑 𝑆 𝑏 ∨ 𝑑 = 𝑏 ) ∧ ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) ) ↔ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( ( 𝑐 𝑅 𝑎 ∨ 𝑐 = 𝑎 ) ∧ ( 𝑑 𝑆 𝑏 ∨ 𝑑 = 𝑏 ) ∧ ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) ) ) ) )
83 df-3an ⊢ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( ( 𝑐 𝑅 𝑎 ∨ 𝑐 = 𝑎 ) ∧ ( 𝑑 𝑆 𝑏 ∨ 𝑑 = 𝑏 ) ∧ ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) ) ) ↔ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( ( 𝑐 𝑅 𝑎 ∨ 𝑐 = 𝑎 ) ∧ ( 𝑑 𝑆 𝑏 ∨ 𝑑 = 𝑏 ) ∧ ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) ) ) )
84 82 83 bitr4di ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) → ( ( ( 𝑐 𝑅 𝑎 ∨ 𝑐 = 𝑎 ) ∧ ( 𝑑 𝑆 𝑏 ∨ 𝑑 = 𝑏 ) ∧ ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) ) ↔ ( ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( ( 𝑐 𝑅 𝑎 ∨ 𝑐 = 𝑎 ) ∧ ( 𝑑 𝑆 𝑏 ∨ 𝑑 = 𝑏 ) ∧ ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) ) ) ) )
85 80 84 bitr2d ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) → ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( ( 𝑐 𝑅 𝑎 ∨ 𝑐 = 𝑎 ) ∧ ( 𝑑 𝑆 𝑏 ∨ 𝑑 = 𝑏 ) ∧ ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) ) ) ↔ ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) )
86 45 85 bitrid ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) → ( ⟨ 𝑐 , 𝑑 ⟩ 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) )
87 44 86 bitr3d ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) → ( ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑐 , 𝑑 ⟩ 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) )
88 41 87 bitrid ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) → ( ⟨ 𝑐 , 𝑑 ⟩ ∈ 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 biimtrid ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑒 ∈ ( 𝐴 × 𝐵 ) → ( 𝑒 ∈ 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 ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) ∖ { ⟨ 𝑋 , 𝑌 ⟩ } ) )