Metamath Proof Explorer

Theorem sexp3

Description: Show that the triple order is set-like. (Contributed by Scott Fenton, 21-Aug-2024)

Ref Expression
Hypotheses xpord3.1 ⊢ 𝑈 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ( ( ( ( 1st ‘ ( 1st ‘ 𝑥 ) ) 𝑅 ( 1st ‘ ( 1st ‘ 𝑦 ) ) ∨ ( 1st ‘ ( 1st ‘ 𝑥 ) ) = ( 1st ‘ ( 1st ‘ 𝑦 ) ) ) ∧ ( ( 2nd ‘ ( 1st ‘ 𝑥 ) ) 𝑆 ( 2nd ‘ ( 1st ‘ 𝑦 ) ) ∨ ( 2nd ‘ ( 1st ‘ 𝑥 ) ) = ( 2nd ‘ ( 1st ‘ 𝑦 ) ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑇 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
sexp3.1 ⊢ ( 𝜑 → 𝑅 Se 𝐴 )
sexp3.2 ⊢ ( 𝜑 → 𝑆 Se 𝐵 )
sexp3.3 ⊢ ( 𝜑 → 𝑇 Se 𝐶 )
Assertion sexp3 ( 𝜑 → 𝑈 Se ( ( 𝐴 × 𝐵 ) × 𝐶 ) )

Proof

Step Hyp Ref Expression
1 xpord3.1 ⊢ 𝑈 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ( ( ( ( 1st ‘ ( 1st ‘ 𝑥 ) ) 𝑅 ( 1st ‘ ( 1st ‘ 𝑦 ) ) ∨ ( 1st ‘ ( 1st ‘ 𝑥 ) ) = ( 1st ‘ ( 1st ‘ 𝑦 ) ) ) ∧ ( ( 2nd ‘ ( 1st ‘ 𝑥 ) ) 𝑆 ( 2nd ‘ ( 1st ‘ 𝑦 ) ) ∨ ( 2nd ‘ ( 1st ‘ 𝑥 ) ) = ( 2nd ‘ ( 1st ‘ 𝑦 ) ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑇 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
2 sexp3.1 ⊢ ( 𝜑 → 𝑅 Se 𝐴 )
3 sexp3.2 ⊢ ( 𝜑 → 𝑆 Se 𝐵 )
4 sexp3.3 ⊢ ( 𝜑 → 𝑇 Se 𝐶 )
5 elxpxp ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ )
6 df-3an ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐶 ) )
7 1 xpord3pred ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) )
8 7 adantl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) )
9 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑎 ∈ 𝐴 )
10 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑅 Se 𝐴 )
11 setlikespec ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑎 ) ∈ V )
12 9 10 11 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → Pred ( 𝑅 , 𝐴 , 𝑎 ) ∈ V )
13 snex ⊢ { 𝑎 } ∈ V
14 13 a1i ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → { 𝑎 } ∈ V )
15 12 14 unexd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∈ V )
16 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑏 ∈ 𝐵 )
17 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑆 Se 𝐵 )
18 setlikespec ⊢ ( ( 𝑏 ∈ 𝐵 ∧ 𝑆 Se 𝐵 ) → Pred ( 𝑆 , 𝐵 , 𝑏 ) ∈ V )
19 16 17 18 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → Pred ( 𝑆 , 𝐵 , 𝑏 ) ∈ V )
20 snex ⊢ { 𝑏 } ∈ V
21 20 a1i ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → { 𝑏 } ∈ V )
22 19 21 unexd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∈ V )
23 15 22 xpexd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∈ V )
24 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑐 ∈ 𝐶 )
25 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑇 Se 𝐶 )
26 setlikespec ⊢ ( ( 𝑐 ∈ 𝐶 ∧ 𝑇 Se 𝐶 ) → Pred ( 𝑇 , 𝐶 , 𝑐 ) ∈ V )
27 24 25 26 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → Pred ( 𝑇 , 𝐶 , 𝑐 ) ∈ V )
28 snex ⊢ { 𝑐 } ∈ V
29 28 a1i ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → { 𝑐 } ∈ V )
30 27 29 unexd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ∈ V )
31 23 30 xpexd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∈ V )
32 31 difexd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ∈ V )
33 8 32 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) ∈ V )
34 predeq3 ⊢ ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) = Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) )
35 34 eleq1d ⊢ ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ → ( Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) ∈ V ↔ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) ∈ V ) )
36 35 biimprd ⊢ ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ → ( Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) ∈ V → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) ∈ V ) )
37 36 com12 ⊢ ( Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) ∈ V → ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) ∈ V ) )
38 33 37 syl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) ∈ V ) )
39 6 38 sylan2br ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) ∈ V ) )
40 39 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑐 ∈ 𝐶 ) → ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) ∈ V ) )
41 40 rexlimdva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ∃ 𝑐 ∈ 𝐶 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) ∈ V ) )
42 41 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) ∈ V ) )
43 5 42 syl5bi ⊢ ( 𝜑 → ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) ∈ V ) )
44 43 ralrimiv ⊢ ( 𝜑 → ∀ 𝑝 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) ∈ V )
45 dfse3 ⊢ ( 𝑈 Se ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ∀ 𝑝 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) ∈ V )
46 44 45 sylibr ⊢ ( 𝜑 → 𝑈 Se ( ( 𝐴 × 𝐵 ) × 𝐶 ) )