Metamath Proof Explorer

Theorem xpord2indlem

Description: Induction over the Cartesian product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 22-Aug-2024)

Ref Expression
Hypotheses xpord2.1 ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ∧ ( ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
xpord2indlem.1 ⊢ 𝑅 Fr 𝐴
xpord2indlem.2 ⊢ 𝑅 Po 𝐴
xpord2indlem.3 ⊢ 𝑅 Se 𝐴
xpord2indlem.4 ⊢ 𝑆 Fr 𝐵
xpord2indlem.5 ⊢ 𝑆 Po 𝐵
xpord2indlem.6 ⊢ 𝑆 Se 𝐵
xpord2indlem.7 ⊢ ( 𝑎 = 𝑐 → ( 𝜑 ↔ 𝜓 ) )
xpord2indlem.8 ⊢ ( 𝑏 = 𝑑 → ( 𝜓 ↔ 𝜒 ) )
xpord2indlem.9 ⊢ ( 𝑎 = 𝑐 → ( 𝜃 ↔ 𝜒 ) )
xpord2indlem.11 ⊢ ( 𝑎 = 𝑋 → ( 𝜑 ↔ 𝜏 ) )
xpord2indlem.12 ⊢ ( 𝑏 = 𝑌 → ( 𝜏 ↔ 𝜂 ) )
xpord2indlem.i ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( ( ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ∧ ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 ∧ ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜃 ) → 𝜑 ) )
Assertion xpord2indlem ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → 𝜂 )

Proof

Step Hyp Ref Expression
1 xpord2.1 ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ∧ ( ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
2 xpord2indlem.1 ⊢ 𝑅 Fr 𝐴
3 xpord2indlem.2 ⊢ 𝑅 Po 𝐴
4 xpord2indlem.3 ⊢ 𝑅 Se 𝐴
5 xpord2indlem.4 ⊢ 𝑆 Fr 𝐵
6 xpord2indlem.5 ⊢ 𝑆 Po 𝐵
7 xpord2indlem.6 ⊢ 𝑆 Se 𝐵
8 xpord2indlem.7 ⊢ ( 𝑎 = 𝑐 → ( 𝜑 ↔ 𝜓 ) )
9 xpord2indlem.8 ⊢ ( 𝑏 = 𝑑 → ( 𝜓 ↔ 𝜒 ) )
10 xpord2indlem.9 ⊢ ( 𝑎 = 𝑐 → ( 𝜃 ↔ 𝜒 ) )
11 xpord2indlem.11 ⊢ ( 𝑎 = 𝑋 → ( 𝜑 ↔ 𝜏 ) )
12 xpord2indlem.12 ⊢ ( 𝑏 = 𝑌 → ( 𝜏 ↔ 𝜂 ) )
13 xpord2indlem.i ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( ( ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ∧ ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 ∧ ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜃 ) → 𝜑 ) )
14 2 a1i ⊢ ( ⊤ → 𝑅 Fr 𝐴 )
15 5 a1i ⊢ ( ⊤ → 𝑆 Fr 𝐵 )
16 1 14 15 frxp2 ⊢ ( ⊤ → 𝑇 Fr ( 𝐴 × 𝐵 ) )
17 3 a1i ⊢ ( ⊤ → 𝑅 Po 𝐴 )
18 6 a1i ⊢ ( ⊤ → 𝑆 Po 𝐵 )
19 1 17 18 poxp2 ⊢ ( ⊤ → 𝑇 Po ( 𝐴 × 𝐵 ) )
20 4 a1i ⊢ ( ⊤ → 𝑅 Se 𝐴 )
21 7 a1i ⊢ ( ⊤ → 𝑆 Se 𝐵 )
22 1 20 21 sexp2 ⊢ ( ⊤ → 𝑇 Se ( 𝐴 × 𝐵 ) )
23 16 19 22 3jca ⊢ ( ⊤ → ( 𝑇 Fr ( 𝐴 × 𝐵 ) ∧ 𝑇 Po ( 𝐴 × 𝐵 ) ∧ 𝑇 Se ( 𝐴 × 𝐵 ) ) )
24 23 mptru ⊢ ( 𝑇 Fr ( 𝐴 × 𝐵 ) ∧ 𝑇 Po ( 𝐴 × 𝐵 ) ∧ 𝑇 Se ( 𝐴 × 𝐵 ) )
25 1 xpord2pred ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) = ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) )
26 25 eleq2d ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( ⟨ 𝑐 , 𝑑 ⟩ ∈ Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) )
27 26 imbi1d ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( ( ⟨ 𝑐 , 𝑑 ⟩ ∈ Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) → 𝜒 ) ↔ ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) → 𝜒 ) ) )
28 eldif ⊢ ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ↔ ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∧ ¬ ⟨ 𝑐 , 𝑑 ⟩ ∈ { ⟨ 𝑎 , 𝑏 ⟩ } ) )
29 opelxp ⊢ ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ↔ ( 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) )
30 opex ⊢ ⟨ 𝑐 , 𝑑 ⟩ ∈ V
31 30 elsn ⊢ ( ⟨ 𝑐 , 𝑑 ⟩ ∈ { ⟨ 𝑎 , 𝑏 ⟩ } ↔ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
32 31 notbii ⊢ ( ¬ ⟨ 𝑐 , 𝑑 ⟩ ∈ { ⟨ 𝑎 , 𝑏 ⟩ } ↔ ¬ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
33 df-ne ⊢ ( ⟨ 𝑐 , 𝑑 ⟩ ≠ ⟨ 𝑎 , 𝑏 ⟩ ↔ ¬ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
34 vex ⊢ 𝑐 ∈ V
35 vex ⊢ 𝑑 ∈ V
36 34 35 opthne ⊢ ( ⟨ 𝑐 , 𝑑 ⟩ ≠ ⟨ 𝑎 , 𝑏 ⟩ ↔ ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) )
37 32 33 36 3bitr2i ⊢ ( ¬ ⟨ 𝑐 , 𝑑 ⟩ ∈ { ⟨ 𝑎 , 𝑏 ⟩ } ↔ ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) )
38 29 37 anbi12i ⊢ ( ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∧ ¬ ⟨ 𝑐 , 𝑑 ⟩ ∈ { ⟨ 𝑎 , 𝑏 ⟩ } ) ↔ ( ( 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∧ ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) ) )
39 28 38 bitri ⊢ ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ↔ ( ( 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∧ ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) ) )
40 39 imbi1i ⊢ ( ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) → 𝜒 ) ↔ ( ( ( 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∧ ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) ) → 𝜒 ) )
41 impexp ⊢ ( ( ( ( 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∧ ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) ) → 𝜒 ) ↔ ( ( 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) → ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) ) )
42 40 41 bitri ⊢ ( ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) → 𝜒 ) ↔ ( ( 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) → ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) ) )
43 27 42 bitrdi ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( ( ⟨ 𝑐 , 𝑑 ⟩ ∈ Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) → 𝜒 ) ↔ ( ( 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) → ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) ) ) )
44 43 2albidv ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( ∀ 𝑐 ∀ 𝑑 ( ⟨ 𝑐 , 𝑑 ⟩ ∈ Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) → 𝜒 ) ↔ ∀ 𝑐 ∀ 𝑑 ( ( 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) → ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) ) ) )
45 r2al ⊢ ( ∀ 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) ↔ ∀ 𝑐 ∀ 𝑑 ( ( 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) → ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) ) )
46 44 45 bitr4di ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( ∀ 𝑐 ∀ 𝑑 ( ⟨ 𝑐 , 𝑑 ⟩ ∈ Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) → 𝜒 ) ↔ ∀ 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) ) )
47 ssun1 ⊢ Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } )
48 ssralv ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) → ( ∀ 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) ) )
49 47 48 ax-mp ⊢ ( ∀ 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) )
50 ssun1 ⊢ Pred ( 𝑆 , 𝐵 , 𝑏 ) ⊆ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } )
51 ssralv ⊢ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ⊆ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) → ( ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) ) )
52 50 51 ax-mp ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) )
53 52 ralimi ⊢ ( ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) )
54 49 53 syl ⊢ ( ∀ 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) )
55 predpoirr ⊢ ( 𝑆 Po 𝐵 → ¬ 𝑏 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) )
56 6 55 ax-mp ⊢ ¬ 𝑏 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 )
57 eleq1w ⊢ ( 𝑑 = 𝑏 → ( 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ↔ 𝑏 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ) )
58 56 57 mtbiri ⊢ ( 𝑑 = 𝑏 → ¬ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) )
59 58 necon2ai ⊢ ( 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) → 𝑑 ≠ 𝑏 )
60 59 olcd ⊢ ( 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) → ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) )
61 pm2.27 ⊢ ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → ( ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → 𝜒 ) )
62 60 61 syl ⊢ ( 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) → ( ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → 𝜒 ) )
63 62 ralimia ⊢ ( ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 )
64 63 ralimi ⊢ ( ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 )
65 54 64 syl ⊢ ( ∀ 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 )
66 ssun2 ⊢ { 𝑏 } ⊆ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } )
67 ssralv ⊢ ( { 𝑏 } ⊆ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) → ( ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → ∀ 𝑑 ∈ { 𝑏 } ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) ) )
68 66 67 ax-mp ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → ∀ 𝑑 ∈ { 𝑏 } ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) )
69 68 ralimi ⊢ ( ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑑 ∈ { 𝑏 } ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) )
70 49 69 syl ⊢ ( ∀ 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑑 ∈ { 𝑏 } ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) )
71 vex ⊢ 𝑏 ∈ V
72 neeq1 ⊢ ( 𝑑 = 𝑏 → ( 𝑑 ≠ 𝑏 ↔ 𝑏 ≠ 𝑏 ) )
73 72 orbi2d ⊢ ( 𝑑 = 𝑏 → ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) ↔ ( 𝑐 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ) ) )
74 9 equcoms ⊢ ( 𝑑 = 𝑏 → ( 𝜓 ↔ 𝜒 ) )
75 74 bicomd ⊢ ( 𝑑 = 𝑏 → ( 𝜒 ↔ 𝜓 ) )
76 73 75 imbi12d ⊢ ( 𝑑 = 𝑏 → ( ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) ↔ ( ( 𝑐 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ) → 𝜓 ) ) )
77 71 76 ralsn ⊢ ( ∀ 𝑑 ∈ { 𝑏 } ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) ↔ ( ( 𝑐 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ) → 𝜓 ) )
78 77 ralbii ⊢ ( ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑑 ∈ { 𝑏 } ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) ↔ ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ) → 𝜓 ) )
79 70 78 sylib ⊢ ( ∀ 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ) → 𝜓 ) )
80 predpoirr ⊢ ( 𝑅 Po 𝐴 → ¬ 𝑎 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) )
81 3 80 ax-mp ⊢ ¬ 𝑎 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 )
82 eleq1w ⊢ ( 𝑐 = 𝑎 → ( 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ↔ 𝑎 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) )
83 81 82 mtbiri ⊢ ( 𝑐 = 𝑎 → ¬ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) )
84 83 necon2ai ⊢ ( 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) → 𝑐 ≠ 𝑎 )
85 84 orcd ⊢ ( 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) → ( 𝑐 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ) )
86 pm2.27 ⊢ ( ( 𝑐 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ) → ( ( ( 𝑐 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ) → 𝜓 ) → 𝜓 ) )
87 85 86 syl ⊢ ( 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) → ( ( ( 𝑐 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ) → 𝜓 ) → 𝜓 ) )
88 87 ralimia ⊢ ( ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ) → 𝜓 ) → ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 )
89 79 88 syl ⊢ ( ∀ 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 )
90 ssun2 ⊢ { 𝑎 } ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } )
91 ssralv ⊢ ( { 𝑎 } ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) → ( ∀ 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → ∀ 𝑐 ∈ { 𝑎 } ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) ) )
92 90 91 ax-mp ⊢ ( ∀ 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → ∀ 𝑐 ∈ { 𝑎 } ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) )
93 52 ralimi ⊢ ( ∀ 𝑐 ∈ { 𝑎 } ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → ∀ 𝑐 ∈ { 𝑎 } ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) )
94 92 93 syl ⊢ ( ∀ 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → ∀ 𝑐 ∈ { 𝑎 } ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) )
95 vex ⊢ 𝑎 ∈ V
96 neeq1 ⊢ ( 𝑐 = 𝑎 → ( 𝑐 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎 ) )
97 96 orbi1d ⊢ ( 𝑐 = 𝑎 → ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) ↔ ( 𝑎 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) ) )
98 10 equcoms ⊢ ( 𝑐 = 𝑎 → ( 𝜃 ↔ 𝜒 ) )
99 98 bicomd ⊢ ( 𝑐 = 𝑎 → ( 𝜒 ↔ 𝜃 ) )
100 97 99 imbi12d ⊢ ( 𝑐 = 𝑎 → ( ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) ↔ ( ( 𝑎 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜃 ) ) )
101 100 ralbidv ⊢ ( 𝑐 = 𝑎 → ( ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) ↔ ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜃 ) ) )
102 95 101 ralsn ⊢ ( ∀ 𝑐 ∈ { 𝑎 } ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) ↔ ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜃 ) )
103 94 102 sylib ⊢ ( ∀ 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜃 ) )
104 59 olcd ⊢ ( 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) → ( 𝑎 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) )
105 pm2.27 ⊢ ( ( 𝑎 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → ( ( ( 𝑎 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜃 ) → 𝜃 ) )
106 104 105 syl ⊢ ( 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) → ( ( ( 𝑎 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜃 ) → 𝜃 ) )
107 106 ralimia ⊢ ( ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜃 )
108 103 107 syl ⊢ ( ∀ 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜃 )
109 65 89 108 3jca ⊢ ( ∀ 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → ( ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ∧ ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 ∧ ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜃 ) )
110 109 13 syl5 ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( ∀ 𝑐 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑑 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ( ( 𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏 ) → 𝜒 ) → 𝜑 ) )
111 46 110 sylbid ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( ∀ 𝑐 ∀ 𝑑 ( ⟨ 𝑐 , 𝑑 ⟩ ∈ Pred ( 𝑇 , ( 𝐴 × 𝐵 ) , ⟨ 𝑎 , 𝑏 ⟩ ) → 𝜒 ) → 𝜑 ) )
112 111 8 9 11 12 frpoins3xpg ⊢ ( ( ( 𝑇 Fr ( 𝐴 × 𝐵 ) ∧ 𝑇 Po ( 𝐴 × 𝐵 ) ∧ 𝑇 Se ( 𝐴 × 𝐵 ) ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) → 𝜂 )
113 24 112 mpan ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → 𝜂 )