sprsymrelf1lem

		Ref	Expression
	Assertion	sprsymrelf1lem	$⊢ (a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \to (\{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\} \to a \subseteq b)$

Proof

Step	Hyp	Ref	Expression
1		prssspr	$⊢ (a \subseteq Pairs (V) \land p \in a) \to \exists i \in V \exists j \in V p = \{i, j\}$
2	1	ad4ant14	$⊢ (((a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \land \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\}) \land p \in a) \to \exists i \in V \exists j \in V p = \{i, j\}$
3		simpr	$⊢ ((i \in V \land j \in V) \land p = \{i, j\}) \to p = \{i, j\}$
4	3	adantr	$⊢ (((i \in V \land j \in V) \land p = \{i, j\}) \land ((a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \land \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\})) \to p = \{i, j\}$
5	4	eleq1d	$⊢ (((i \in V \land j \in V) \land p = \{i, j\}) \land ((a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \land \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\})) \to (p \in a \leftrightarrow \{i, j\} \in a)$
6		simpr	$⊢ (((i \in V \land j \in V) \land p = \{i, j\}) \land \{i, j\} \in a) \to \{i, j\} \in a$
7		eqeq1	$⊢ c = \{i, j\} \to (c = \{i, j\} \leftrightarrow \{i, j\} = \{i, j\})$
8	7	adantl	$⊢ ((((i \in V \land j \in V) \land p = \{i, j\}) \land \{i, j\} \in a) \land c = \{i, j\}) \to (c = \{i, j\} \leftrightarrow \{i, j\} = \{i, j\})$
9		eqidd	$⊢ (((i \in V \land j \in V) \land p = \{i, j\}) \land \{i, j\} \in a) \to \{i, j\} = \{i, j\}$
10	6 8 9	rspcedvd	$⊢ (((i \in V \land j \in V) \land p = \{i, j\}) \land \{i, j\} \in a) \to \exists c \in a c = \{i, j\}$
11	10	adantlr	$⊢ ((((i \in V \land j \in V) \land p = \{i, j\}) \land ((a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \land \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\})) \land \{i, j\} \in a) \to \exists c \in a c = \{i, j\}$
12		preq12	$⊢ (x = i \land y = j) \to \{x, y\} = \{i, j\}$
13	12	eqeq2d	$⊢ (x = i \land y = j) \to (c = \{x, y\} \leftrightarrow c = \{i, j\})$
14	13	rexbidv	$⊢ (x = i \land y = j) \to (\exists c \in a c = \{x, y\} \leftrightarrow \exists c \in a c = \{i, j\})$
15	14	opelopabga	$⊢ (i \in V \land j \in V) \to (⟨i, j⟩ \in \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} \leftrightarrow \exists c \in a c = \{i, j\})$
16	15	bicomd	$⊢ (i \in V \land j \in V) \to (\exists c \in a c = \{i, j\} \leftrightarrow ⟨i, j⟩ \in \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\})$
17	16	ad3antrrr	$⊢ ((((i \in V \land j \in V) \land p = \{i, j\}) \land ((a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \land \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\})) \land \{i, j\} \in a) \to (\exists c \in a c = \{i, j\} \leftrightarrow ⟨i, j⟩ \in \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\})$
18	11 17	mpbid	$⊢ ((((i \in V \land j \in V) \land p = \{i, j\}) \land ((a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \land \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\})) \land \{i, j\} \in a) \to ⟨i, j⟩ \in \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\}$
19	18	ex	$⊢ (((i \in V \land j \in V) \land p = \{i, j\}) \land ((a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \land \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\})) \to (\{i, j\} \in a \to ⟨i, j⟩ \in \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\})$
20	5 19	sylbid	$⊢ (((i \in V \land j \in V) \land p = \{i, j\}) \land ((a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \land \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\})) \to (p \in a \to ⟨i, j⟩ \in \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\})$
21		eleq2	$⊢ \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\} \to (⟨i, j⟩ \in \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} \leftrightarrow ⟨i, j⟩ \in \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\})$
22	21	ad2antll	$⊢ (((i \in V \land j \in V) \land p = \{i, j\}) \land ((a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \land \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\})) \to (⟨i, j⟩ \in \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} \leftrightarrow ⟨i, j⟩ \in \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\})$
23	13	rexbidv	$⊢ (x = i \land y = j) \to (\exists c \in b c = \{x, y\} \leftrightarrow \exists c \in b c = \{i, j\})$
24	23	opelopabga	$⊢ (i \in V \land j \in V) \to (⟨i, j⟩ \in \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\} \leftrightarrow \exists c \in b c = \{i, j\})$
25	24	el2v	$⊢ ⟨i, j⟩ \in \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\} \leftrightarrow \exists c \in b c = \{i, j\}$
26		eqtr3	$⊢ (p = \{i, j\} \land c = \{i, j\}) \to p = c$
27	26	equcomd	$⊢ (p = \{i, j\} \land c = \{i, j\}) \to c = p$
28	27	eleq1d	$⊢ (p = \{i, j\} \land c = \{i, j\}) \to (c \in b \leftrightarrow p \in b)$
29	28	biimpd	$⊢ (p = \{i, j\} \land c = \{i, j\}) \to (c \in b \to p \in b)$
30	29	ex	$⊢ p = \{i, j\} \to (c = \{i, j\} \to (c \in b \to p \in b))$
31	30	com13	$⊢ c \in b \to (c = \{i, j\} \to (p = \{i, j\} \to p \in b))$
32	31	imp	$⊢ (c \in b \land c = \{i, j\}) \to (p = \{i, j\} \to p \in b)$
33	32	rexlimiva	$⊢ \exists c \in b c = \{i, j\} \to (p = \{i, j\} \to p \in b)$
34	33	com12	$⊢ p = \{i, j\} \to (\exists c \in b c = \{i, j\} \to p \in b)$
35	34	adantl	$⊢ ((i \in V \land j \in V) \land p = \{i, j\}) \to (\exists c \in b c = \{i, j\} \to p \in b)$
36	35	adantr	$⊢ (((i \in V \land j \in V) \land p = \{i, j\}) \land ((a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \land \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\})) \to (\exists c \in b c = \{i, j\} \to p \in b)$
37	25 36	syl5bi	$⊢ (((i \in V \land j \in V) \land p = \{i, j\}) \land ((a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \land \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\})) \to (⟨i, j⟩ \in \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\} \to p \in b)$
38	22 37	sylbid	$⊢ (((i \in V \land j \in V) \land p = \{i, j\}) \land ((a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \land \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\})) \to (⟨i, j⟩ \in \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} \to p \in b)$
39	20 38	syld	$⊢ (((i \in V \land j \in V) \land p = \{i, j\}) \land ((a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \land \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\})) \to (p \in a \to p \in b)$
40	39	expimpd	$⊢ ((i \in V \land j \in V) \land p = \{i, j\}) \to ((((a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \land \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\}) \land p \in a) \to p \in b)$
41	40	rexlimdva2	$⊢ i \in V \to (\exists j \in V p = \{i, j\} \to ((((a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \land \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\}) \land p \in a) \to p \in b))$
42	41	rexlimiv	$⊢ \exists i \in V \exists j \in V p = \{i, j\} \to ((((a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \land \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\}) \land p \in a) \to p \in b)$
43	2 42	mpcom	$⊢ (((a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \land \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\}) \land p \in a) \to p \in b$
44	43	ex	$⊢ ((a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \land \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\}) \to (p \in a \to p \in b)$
45	44	ssrdv	$⊢ ((a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \land \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\}) \to a \subseteq b$
46	45	ex	$⊢ (a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \to (\{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\} \to a \subseteq b)$

Metamath Proof Explorer

Theorem sprsymrelf1lem

Proof