Metamath Proof Explorer


Theorem xpord2ind

Description: Induction over the cross 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𝑦 ) ) ∧ 𝑥𝑦 ) ) }
xpord2ind.1 𝑅 Fr 𝐴
xpord2ind.2 𝑅 Po 𝐴
xpord2ind.3 𝑅 Se 𝐴
xpord2ind.4 𝑆 Fr 𝐵
xpord2ind.5 𝑆 Po 𝐵
xpord2ind.6 𝑆 Se 𝐵
xpord2ind.7 ( 𝑎 = 𝑐 → ( 𝜑𝜓 ) )
xpord2ind.8 ( 𝑏 = 𝑑 → ( 𝜓𝜒 ) )
xpord2ind.9 ( 𝑎 = 𝑐 → ( 𝜃𝜒 ) )
xpord2ind.11 ( 𝑎 = 𝑋 → ( 𝜑𝜏 ) )
xpord2ind.12 ( 𝑏 = 𝑌 → ( 𝜏𝜂 ) )
xpord2ind.i ( ( 𝑎𝐴𝑏𝐵 ) → ( ( ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ∧ ∀ 𝑐 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 ∧ ∀ 𝑑 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜃 ) → 𝜑 ) )
Assertion xpord2ind ( ( 𝑋𝐴𝑌𝐵 ) → 𝜂 )

Proof

Step Hyp Ref Expression
1 xpord2.1 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ∧ ( ( ( 1st𝑥 ) 𝑅 ( 1st𝑦 ) ∨ ( 1st𝑥 ) = ( 1st𝑦 ) ) ∧ ( ( 2nd𝑥 ) 𝑆 ( 2nd𝑦 ) ∨ ( 2nd𝑥 ) = ( 2nd𝑦 ) ) ∧ 𝑥𝑦 ) ) }
2 xpord2ind.1 𝑅 Fr 𝐴
3 xpord2ind.2 𝑅 Po 𝐴
4 xpord2ind.3 𝑅 Se 𝐴
5 xpord2ind.4 𝑆 Fr 𝐵
6 xpord2ind.5 𝑆 Po 𝐵
7 xpord2ind.6 𝑆 Se 𝐵
8 xpord2ind.7 ( 𝑎 = 𝑐 → ( 𝜑𝜓 ) )
9 xpord2ind.8 ( 𝑏 = 𝑑 → ( 𝜓𝜒 ) )
10 xpord2ind.9 ( 𝑎 = 𝑐 → ( 𝜃𝜒 ) )
11 xpord2ind.11 ( 𝑎 = 𝑋 → ( 𝜑𝜏 ) )
12 xpord2ind.12 ( 𝑏 = 𝑌 → ( 𝜏𝜂 ) )
13 xpord2ind.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 ( ( 𝑋𝐴𝑌𝐵 ) → 𝜂 )