sexp2

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

	Ref	Expression
Hypotheses	xpord2.1	$⊢ T = \{⟨x, y⟩ \| (x \in (A \times B) \land y \in (A \times B) \land ((1^{st} (x) R 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) S 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}$
	sexp2.1	$⊢ φ \to R Se A$
	sexp2.2	$⊢ φ \to S Se B$
Assertion	sexp2	$⊢ φ \to T Se (A \times B)$

Proof

Step	Hyp	Ref	Expression
1		xpord2.1	$⊢ T = \{⟨x, y⟩ \| (x \in (A \times B) \land y \in (A \times B) \land ((1^{st} (x) R 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) S 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}$
2		sexp2.1	$⊢ φ \to R Se A$
3		sexp2.2	$⊢ φ \to S Se B$
4		elxp2	$⊢ p \in (A \times B) \leftrightarrow \exists a \in A \exists b \in B p = ⟨a, b⟩$
5	1	xpord2pred	$⊢ (a \in A \land b \in B) \to Pred (T, (A \times B), ⟨a, b⟩) = ((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\}$
6	5	adantl	$⊢ (φ \land (a \in A \land b \in B)) \to Pred (T, (A \times B), ⟨a, b⟩) = ((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\}$
7		setlikespec	$⊢ (a \in A \land R Se A) \to Pred (R, A, a) \in V$
8	7	ancoms	$⊢ (R Se A \land a \in A) \to Pred (R, A, a) \in V$
9	2 8	sylan	$⊢ (φ \land a \in A) \to Pred (R, A, a) \in V$
10	9	adantrr	$⊢ (φ \land (a \in A \land b \in B)) \to Pred (R, A, a) \in V$
11		vsnex	$⊢ \{a\} \in V$
12	11	a1i	$⊢ (φ \land (a \in A \land b \in B)) \to \{a\} \in V$
13	10 12	unexd	$⊢ (φ \land (a \in A \land b \in B)) \to Pred (R, A, a) \cup \{a\} \in V$
14		setlikespec	$⊢ (b \in B \land S Se B) \to Pred (S, B, b) \in V$
15	14	ancoms	$⊢ (S Se B \land b \in B) \to Pred (S, B, b) \in V$
16	3 15	sylan	$⊢ (φ \land b \in B) \to Pred (S, B, b) \in V$
17	16	adantrl	$⊢ (φ \land (a \in A \land b \in B)) \to Pred (S, B, b) \in V$
18		vsnex	$⊢ \{b\} \in V$
19	18	a1i	$⊢ (φ \land (a \in A \land b \in B)) \to \{b\} \in V$
20	17 19	unexd	$⊢ (φ \land (a \in A \land b \in B)) \to Pred (S, B, b) \cup \{b\} \in V$
21	13 20	xpexd	$⊢ (φ \land (a \in A \land b \in B)) \to (Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\}) \in V$
22	21	difexd	$⊢ (φ \land (a \in A \land b \in B)) \to ((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\} \in V$
23	6 22	eqeltrd	$⊢ (φ \land (a \in A \land b \in B)) \to Pred (T, (A \times B), ⟨a, b⟩) \in V$
24		predeq3	$⊢ p = ⟨a, b⟩ \to Pred (T, (A \times B), p) = Pred (T, (A \times B), ⟨a, b⟩)$
25	24	eleq1d	$⊢ p = ⟨a, b⟩ \to (Pred (T, (A \times B), p) \in V \leftrightarrow Pred (T, (A \times B), ⟨a, b⟩) \in V)$
26	23 25	syl5ibrcom	$⊢ (φ \land (a \in A \land b \in B)) \to (p = ⟨a, b⟩ \to Pred (T, (A \times B), p) \in V)$
27	26	rexlimdvva	$⊢ φ \to (\exists a \in A \exists b \in B p = ⟨a, b⟩ \to Pred (T, (A \times B), p) \in V)$
28	4 27	biimtrid	$⊢ φ \to (p \in (A \times B) \to Pred (T, (A \times B), p) \in V)$
29	28	ralrimiv	$⊢ φ \to \forall p \in (A \times B) Pred (T, (A \times B), p) \in V$
30		dfse3	$⊢ T Se (A \times B) \leftrightarrow \forall p \in (A \times B) Pred (T, (A \times B), p) \in V$
31	29 30	sylibr	$⊢ φ \to T Se (A \times B)$

Metamath Proof Explorer

Theorem sexp2

Proof