Metamath Proof Explorer


Theorem sexp2

Description: Condition for the relationship in frxp2 to be set-like. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Hypotheses xpord2.1 T = x y | x A × B y A × B 1 st x R 1 st y 1 st x = 1 st y 2 nd x S 2 nd y 2 nd x = 2 nd y x y
sexp2.1 φ R Se A
sexp2.2 φ S Se B
Assertion sexp2 φ T Se A × B

Proof

Step Hyp Ref Expression
1 xpord2.1 T = x y | x A × B y A × B 1 st x R 1 st y 1 st x = 1 st y 2 nd x S 2 nd y 2 nd x = 2 nd y x y
2 sexp2.1 φ R Se A
3 sexp2.2 φ S Se B
4 elxp2 p A × B a A b B p = a b
5 1 xpord2pred a A b B Pred T A × B a b = Pred R A a a × Pred S B b b a b
6 5 adantl φ a A b B Pred T A × B a b = Pred R A a a × Pred S B b b a b
7 setlikespec a A R Se A Pred R A a V
8 7 ancoms R Se A a A Pred R A a V
9 2 8 sylan φ a A Pred R A a V
10 9 adantrr φ a A b B Pred R A a V
11 snex a V
12 11 a1i φ a A b B a V
13 10 12 unexd φ a A b B Pred R A a a V
14 setlikespec b B S Se B Pred S B b V
15 14 ancoms S Se B b B Pred S B b V
16 3 15 sylan φ b B Pred S B b V
17 16 adantrl φ a A b B Pred S B b V
18 snex b V
19 18 a1i φ a A b B b V
20 17 19 unexd φ a A b B Pred S B b b V
21 13 20 xpexd φ a A b B Pred R A a a × Pred S B b b V
22 21 difexd φ a A b B Pred R A a a × Pred S B b b a b V
23 6 22 eqeltrd φ a A b B Pred T A × B a b V
24 predeq3 p = a b Pred T A × B p = Pred T A × B a b
25 24 eleq1d p = a b Pred T A × B p V Pred T A × B a b V
26 23 25 syl5ibrcom φ a A b B p = a b Pred T A × B p V
27 26 rexlimdvva φ a A b B p = a b Pred T A × B p V
28 4 27 syl5bi φ p A × B Pred T A × B p V
29 28 ralrimiv φ p A × B Pred T A × B p V
30 dfse3 T Se A × B p A × B Pred T A × B p V
31 29 30 sylibr φ T Se A × B