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 U = x y | x A × B × C y A × B × C 1 st 1 st x R 1 st 1 st y 1 st 1 st x = 1 st 1 st y 2 nd 1 st x S 2 nd 1 st y 2 nd 1 st x = 2 nd 1 st y 2 nd x T 2 nd y 2 nd x = 2 nd y x y
sexp3.1 φ R Se A
sexp3.2 φ S Se B
sexp3.3 φ T Se C
Assertion sexp3 φ U Se A × B × C

Proof

Step Hyp Ref Expression
1 xpord3.1 U = x y | x A × B × C y A × B × C 1 st 1 st x R 1 st 1 st y 1 st 1 st x = 1 st 1 st y 2 nd 1 st x S 2 nd 1 st y 2 nd 1 st x = 2 nd 1 st y 2 nd x T 2 nd y 2 nd x = 2 nd y x y
2 sexp3.1 φ R Se A
3 sexp3.2 φ S Se B
4 sexp3.3 φ T Se C
5 elxpxp p A × B × C a A b B c C p = a b c
6 df-3an a A b B c C a A b B c C
7 1 xpord3pred a A b B c C Pred U A × B × C a b c = Pred R A a a × Pred S B b b × Pred T C c c a b c
8 7 adantl φ a A b B c C Pred U A × B × C a b c = Pred R A a a × Pred S B b b × Pred T C c c a b c
9 simpr1 φ a A b B c C a A
10 2 adantr φ a A b B c C R Se A
11 setlikespec a A R Se A Pred R A a V
12 9 10 11 syl2anc φ a A b B c C Pred R A a V
13 snex a V
14 13 a1i φ a A b B c C a V
15 12 14 unexd φ a A b B c C Pred R A a a V
16 simpr2 φ a A b B c C b B
17 3 adantr φ a A b B c C S Se B
18 setlikespec b B S Se B Pred S B b V
19 16 17 18 syl2anc φ a A b B c C Pred S B b V
20 snex b V
21 20 a1i φ a A b B c C b V
22 19 21 unexd φ a A b B c C Pred S B b b V
23 15 22 xpexd φ a A b B c C Pred R A a a × Pred S B b b V
24 simpr3 φ a A b B c C c C
25 4 adantr φ a A b B c C T Se C
26 setlikespec c C T Se C Pred T C c V
27 24 25 26 syl2anc φ a A b B c C Pred T C c V
28 snex c V
29 28 a1i φ a A b B c C c V
30 27 29 unexd φ a A b B c C Pred T C c c V
31 23 30 xpexd φ a A b B c C Pred R A a a × Pred S B b b × Pred T C c c V
32 31 difexd φ a A b B c C Pred R A a a × Pred S B b b × Pred T C c c a b c V
33 8 32 eqeltrd φ a A b B c C Pred U A × B × C a b c V
34 predeq3 p = a b c Pred U A × B × C p = Pred U A × B × C a b c
35 34 eleq1d p = a b c Pred U A × B × C p V Pred U A × B × C a b c V
36 35 biimprd p = a b c Pred U A × B × C a b c V Pred U A × B × C p V
37 36 com12 Pred U A × B × C a b c V p = a b c Pred U A × B × C p V
38 33 37 syl φ a A b B c C p = a b c Pred U A × B × C p V
39 6 38 sylan2br φ a A b B c C p = a b c Pred U A × B × C p V
40 39 anassrs φ a A b B c C p = a b c Pred U A × B × C p V
41 40 rexlimdva φ a A b B c C p = a b c Pred U A × B × C p V
42 41 rexlimdvva φ a A b B c C p = a b c Pred U A × B × C p V
43 5 42 syl5bi φ p A × B × C Pred U A × B × C p V
44 43 ralrimiv φ p A × B × C Pred U A × B × C p V
45 dfse3 U Se A × B × C p A × B × C Pred U A × B × C p V
46 44 45 sylibr φ U Se A × B × C