tpres

Description: An unordered triple of ordered pairs restricted to all but one first components of the pairs is an unordered pair of ordered pairs. (Contributed by AV, 14-Mar-2020)

	Ref	Expression
Hypotheses	tpres.t	$⊢ φ \to T = \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\}$
	tpres.b	$⊢ φ \to B \in V$
	tpres.c	$⊢ φ \to C \in V$
	tpres.e	$⊢ φ \to E \in V$
	tpres.f	$⊢ φ \to F \in V$
	tpres.1	$⊢ φ \to B \neq A$
	tpres.2	$⊢ φ \to C \neq A$
Assertion	tpres	$⊢ φ \to {T ↾}_{(V ∖ \{A\})} = \{⟨B, E⟩, ⟨C, F⟩\}$

Proof

Step	Hyp	Ref	Expression
1		tpres.t	$⊢ φ \to T = \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\}$
2		tpres.b	$⊢ φ \to B \in V$
3		tpres.c	$⊢ φ \to C \in V$
4		tpres.e	$⊢ φ \to E \in V$
5		tpres.f	$⊢ φ \to F \in V$
6		tpres.1	$⊢ φ \to B \neq A$
7		tpres.2	$⊢ φ \to C \neq A$
8		df-res	$⊢ {T ↾}_{(V ∖ \{A\})} = T \cap ((V ∖ \{A\}) \times V)$
9		elin	$⊢ x \in (T \cap ((V ∖ \{A\}) \times V)) \leftrightarrow (x \in T \land x \in ((V ∖ \{A\}) \times V))$
10		elxp	$⊢ x \in ((V ∖ \{A\}) \times V) \leftrightarrow \exists a \exists b (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V))$
11	10	anbi2i	$⊢ (x \in T \land x \in ((V ∖ \{A\}) \times V)) \leftrightarrow (x \in T \land \exists a \exists b (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V)))$
12	1	eleq2d	$⊢ φ \to (x \in T \leftrightarrow x \in \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\})$
13		vex	$⊢ x \in V$
14	13	eltp	$⊢ x \in \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} \leftrightarrow (x = ⟨A, D⟩ \lor x = ⟨B, E⟩ \lor x = ⟨C, F⟩)$
15		eldifsn	$⊢ a \in (V ∖ \{A\}) \leftrightarrow (a \in V \land a \neq A)$
16		eqeq1	$⊢ x = ⟨a, b⟩ \to (x = ⟨A, D⟩ \leftrightarrow ⟨a, b⟩ = ⟨A, D⟩)$
17	16	adantl	$⊢ (a \neq A \land x = ⟨a, b⟩) \to (x = ⟨A, D⟩ \leftrightarrow ⟨a, b⟩ = ⟨A, D⟩)$
18		vex	$⊢ a \in V$
19		vex	$⊢ b \in V$
20	18 19	opth	$⊢ ⟨a, b⟩ = ⟨A, D⟩ \leftrightarrow (a = A \land b = D)$
21		eqneqall	$⊢ a = A \to (a \neq A \to (b = D \to (φ \to (x = ⟨B, E⟩ \lor x = ⟨C, F⟩))))$
22	21	com12	$⊢ a \neq A \to (a = A \to (b = D \to (φ \to (x = ⟨B, E⟩ \lor x = ⟨C, F⟩))))$
23	22	impd	$⊢ a \neq A \to ((a = A \land b = D) \to (φ \to (x = ⟨B, E⟩ \lor x = ⟨C, F⟩)))$
24	20 23	syl5bi	$⊢ a \neq A \to (⟨a, b⟩ = ⟨A, D⟩ \to (φ \to (x = ⟨B, E⟩ \lor x = ⟨C, F⟩)))$
25	24	adantr	$⊢ (a \neq A \land x = ⟨a, b⟩) \to (⟨a, b⟩ = ⟨A, D⟩ \to (φ \to (x = ⟨B, E⟩ \lor x = ⟨C, F⟩)))$
26	17 25	sylbid	$⊢ (a \neq A \land x = ⟨a, b⟩) \to (x = ⟨A, D⟩ \to (φ \to (x = ⟨B, E⟩ \lor x = ⟨C, F⟩)))$
27	26	impd	$⊢ (a \neq A \land x = ⟨a, b⟩) \to ((x = ⟨A, D⟩ \land φ) \to (x = ⟨B, E⟩ \lor x = ⟨C, F⟩))$
28	27	ex	$⊢ a \neq A \to (x = ⟨a, b⟩ \to ((x = ⟨A, D⟩ \land φ) \to (x = ⟨B, E⟩ \lor x = ⟨C, F⟩)))$
29	28	adantl	$⊢ (a \in V \land a \neq A) \to (x = ⟨a, b⟩ \to ((x = ⟨A, D⟩ \land φ) \to (x = ⟨B, E⟩ \lor x = ⟨C, F⟩)))$
30	15 29	sylbi	$⊢ a \in (V ∖ \{A\}) \to (x = ⟨a, b⟩ \to ((x = ⟨A, D⟩ \land φ) \to (x = ⟨B, E⟩ \lor x = ⟨C, F⟩)))$
31	30	adantr	$⊢ (a \in (V ∖ \{A\}) \land b \in V) \to (x = ⟨a, b⟩ \to ((x = ⟨A, D⟩ \land φ) \to (x = ⟨B, E⟩ \lor x = ⟨C, F⟩)))$
32	31	impcom	$⊢ (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V)) \to ((x = ⟨A, D⟩ \land φ) \to (x = ⟨B, E⟩ \lor x = ⟨C, F⟩))$
33	32	com12	$⊢ (x = ⟨A, D⟩ \land φ) \to ((x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V)) \to (x = ⟨B, E⟩ \lor x = ⟨C, F⟩))$
34	33	exlimdvv	$⊢ (x = ⟨A, D⟩ \land φ) \to (\exists a \exists b (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V)) \to (x = ⟨B, E⟩ \lor x = ⟨C, F⟩))$
35	34	ex	$⊢ x = ⟨A, D⟩ \to (φ \to (\exists a \exists b (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V)) \to (x = ⟨B, E⟩ \lor x = ⟨C, F⟩)))$
36	35	impd	$⊢ x = ⟨A, D⟩ \to ((φ \land \exists a \exists b (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V))) \to (x = ⟨B, E⟩ \lor x = ⟨C, F⟩))$
37		orc	$⊢ x = ⟨B, E⟩ \to (x = ⟨B, E⟩ \lor x = ⟨C, F⟩)$
38	37	a1d	$⊢ x = ⟨B, E⟩ \to ((φ \land \exists a \exists b (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V))) \to (x = ⟨B, E⟩ \lor x = ⟨C, F⟩))$
39		olc	$⊢ x = ⟨C, F⟩ \to (x = ⟨B, E⟩ \lor x = ⟨C, F⟩)$
40	39	a1d	$⊢ x = ⟨C, F⟩ \to ((φ \land \exists a \exists b (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V))) \to (x = ⟨B, E⟩ \lor x = ⟨C, F⟩))$
41	36 38 40	3jaoi	$⊢ (x = ⟨A, D⟩ \lor x = ⟨B, E⟩ \lor x = ⟨C, F⟩) \to ((φ \land \exists a \exists b (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V))) \to (x = ⟨B, E⟩ \lor x = ⟨C, F⟩))$
42	14 41	sylbi	$⊢ x \in \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} \to ((φ \land \exists a \exists b (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V))) \to (x = ⟨B, E⟩ \lor x = ⟨C, F⟩))$
43	13	elpr	$⊢ x \in \{⟨B, E⟩, ⟨C, F⟩\} \leftrightarrow (x = ⟨B, E⟩ \lor x = ⟨C, F⟩)$
44	42 43	syl6ibr	$⊢ x \in \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} \to ((φ \land \exists a \exists b (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V))) \to x \in \{⟨B, E⟩, ⟨C, F⟩\})$
45	44	expd	$⊢ x \in \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} \to (φ \to (\exists a \exists b (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V)) \to x \in \{⟨B, E⟩, ⟨C, F⟩\}))$
46	45	com12	$⊢ φ \to (x \in \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} \to (\exists a \exists b (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V)) \to x \in \{⟨B, E⟩, ⟨C, F⟩\}))$
47	12 46	sylbid	$⊢ φ \to (x \in T \to (\exists a \exists b (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V)) \to x \in \{⟨B, E⟩, ⟨C, F⟩\}))$
48	47	impd	$⊢ φ \to ((x \in T \land \exists a \exists b (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V))) \to x \in \{⟨B, E⟩, ⟨C, F⟩\})$
49		3mix2	$⊢ x = ⟨B, E⟩ \to (x = ⟨A, D⟩ \lor x = ⟨B, E⟩ \lor x = ⟨C, F⟩)$
50		3mix3	$⊢ x = ⟨C, F⟩ \to (x = ⟨A, D⟩ \lor x = ⟨B, E⟩ \lor x = ⟨C, F⟩)$
51	49 50	jaoi	$⊢ (x = ⟨B, E⟩ \lor x = ⟨C, F⟩) \to (x = ⟨A, D⟩ \lor x = ⟨B, E⟩ \lor x = ⟨C, F⟩)$
52	51	adantr	$⊢ ((x = ⟨B, E⟩ \lor x = ⟨C, F⟩) \land φ) \to (x = ⟨A, D⟩ \lor x = ⟨B, E⟩ \lor x = ⟨C, F⟩)$
53	12 14	bitrdi	$⊢ φ \to (x \in T \leftrightarrow (x = ⟨A, D⟩ \lor x = ⟨B, E⟩ \lor x = ⟨C, F⟩))$
54	53	adantl	$⊢ ((x = ⟨B, E⟩ \lor x = ⟨C, F⟩) \land φ) \to (x \in T \leftrightarrow (x = ⟨A, D⟩ \lor x = ⟨B, E⟩ \lor x = ⟨C, F⟩))$
55	52 54	mpbird	$⊢ ((x = ⟨B, E⟩ \lor x = ⟨C, F⟩) \land φ) \to x \in T$
56	2	elexd	$⊢ φ \to B \in V$
57	4	elexd	$⊢ φ \to E \in V$
58	56 6 57	jca31	$⊢ φ \to ((B \in V \land B \neq A) \land E \in V)$
59	58	anim2i	$⊢ (x = ⟨B, E⟩ \land φ) \to (x = ⟨B, E⟩ \land ((B \in V \land B \neq A) \land E \in V))$
60		opeq12	$⊢ (a = B \land b = E) \to ⟨a, b⟩ = ⟨B, E⟩$
61	60	eqeq2d	$⊢ (a = B \land b = E) \to (x = ⟨a, b⟩ \leftrightarrow x = ⟨B, E⟩)$
62		eleq1	$⊢ a = B \to (a \in V \leftrightarrow B \in V)$
63		neeq1	$⊢ a = B \to (a \neq A \leftrightarrow B \neq A)$
64	62 63	anbi12d	$⊢ a = B \to ((a \in V \land a \neq A) \leftrightarrow (B \in V \land B \neq A))$
65		eleq1	$⊢ b = E \to (b \in V \leftrightarrow E \in V)$
66	64 65	bi2anan9	$⊢ (a = B \land b = E) \to (((a \in V \land a \neq A) \land b \in V) \leftrightarrow ((B \in V \land B \neq A) \land E \in V))$
67	61 66	anbi12d	$⊢ (a = B \land b = E) \to ((x = ⟨a, b⟩ \land ((a \in V \land a \neq A) \land b \in V)) \leftrightarrow (x = ⟨B, E⟩ \land ((B \in V \land B \neq A) \land E \in V)))$
68	67	spc2egv	$⊢ (B \in V \land E \in V) \to ((x = ⟨B, E⟩ \land ((B \in V \land B \neq A) \land E \in V)) \to \exists a \exists b (x = ⟨a, b⟩ \land ((a \in V \land a \neq A) \land b \in V)))$
69	2 4 68	syl2anc	$⊢ φ \to ((x = ⟨B, E⟩ \land ((B \in V \land B \neq A) \land E \in V)) \to \exists a \exists b (x = ⟨a, b⟩ \land ((a \in V \land a \neq A) \land b \in V)))$
70	69	adantl	$⊢ (x = ⟨B, E⟩ \land φ) \to ((x = ⟨B, E⟩ \land ((B \in V \land B \neq A) \land E \in V)) \to \exists a \exists b (x = ⟨a, b⟩ \land ((a \in V \land a \neq A) \land b \in V)))$
71	59 70	mpd	$⊢ (x = ⟨B, E⟩ \land φ) \to \exists a \exists b (x = ⟨a, b⟩ \land ((a \in V \land a \neq A) \land b \in V))$
72	3	elexd	$⊢ φ \to C \in V$
73	5	elexd	$⊢ φ \to F \in V$
74	72 7 73	jca31	$⊢ φ \to ((C \in V \land C \neq A) \land F \in V)$
75	74	anim2i	$⊢ (x = ⟨C, F⟩ \land φ) \to (x = ⟨C, F⟩ \land ((C \in V \land C \neq A) \land F \in V))$
76		opeq12	$⊢ (a = C \land b = F) \to ⟨a, b⟩ = ⟨C, F⟩$
77	76	eqeq2d	$⊢ (a = C \land b = F) \to (x = ⟨a, b⟩ \leftrightarrow x = ⟨C, F⟩)$
78		eleq1	$⊢ a = C \to (a \in V \leftrightarrow C \in V)$
79		neeq1	$⊢ a = C \to (a \neq A \leftrightarrow C \neq A)$
80	78 79	anbi12d	$⊢ a = C \to ((a \in V \land a \neq A) \leftrightarrow (C \in V \land C \neq A))$
81		eleq1	$⊢ b = F \to (b \in V \leftrightarrow F \in V)$
82	80 81	bi2anan9	$⊢ (a = C \land b = F) \to (((a \in V \land a \neq A) \land b \in V) \leftrightarrow ((C \in V \land C \neq A) \land F \in V))$
83	77 82	anbi12d	$⊢ (a = C \land b = F) \to ((x = ⟨a, b⟩ \land ((a \in V \land a \neq A) \land b \in V)) \leftrightarrow (x = ⟨C, F⟩ \land ((C \in V \land C \neq A) \land F \in V)))$
84	83	spc2egv	$⊢ (C \in V \land F \in V) \to ((x = ⟨C, F⟩ \land ((C \in V \land C \neq A) \land F \in V)) \to \exists a \exists b (x = ⟨a, b⟩ \land ((a \in V \land a \neq A) \land b \in V)))$
85	3 5 84	syl2anc	$⊢ φ \to ((x = ⟨C, F⟩ \land ((C \in V \land C \neq A) \land F \in V)) \to \exists a \exists b (x = ⟨a, b⟩ \land ((a \in V \land a \neq A) \land b \in V)))$
86	85	adantl	$⊢ (x = ⟨C, F⟩ \land φ) \to ((x = ⟨C, F⟩ \land ((C \in V \land C \neq A) \land F \in V)) \to \exists a \exists b (x = ⟨a, b⟩ \land ((a \in V \land a \neq A) \land b \in V)))$
87	75 86	mpd	$⊢ (x = ⟨C, F⟩ \land φ) \to \exists a \exists b (x = ⟨a, b⟩ \land ((a \in V \land a \neq A) \land b \in V))$
88	71 87	jaoian	$⊢ ((x = ⟨B, E⟩ \lor x = ⟨C, F⟩) \land φ) \to \exists a \exists b (x = ⟨a, b⟩ \land ((a \in V \land a \neq A) \land b \in V))$
89	15	anbi1i	$⊢ (a \in (V ∖ \{A\}) \land b \in V) \leftrightarrow ((a \in V \land a \neq A) \land b \in V)$
90	89	anbi2i	$⊢ (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V)) \leftrightarrow (x = ⟨a, b⟩ \land ((a \in V \land a \neq A) \land b \in V))$
91	90	2exbii	$⊢ \exists a \exists b (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V)) \leftrightarrow \exists a \exists b (x = ⟨a, b⟩ \land ((a \in V \land a \neq A) \land b \in V))$
92	88 91	sylibr	$⊢ ((x = ⟨B, E⟩ \lor x = ⟨C, F⟩) \land φ) \to \exists a \exists b (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V))$
93	55 92	jca	$⊢ ((x = ⟨B, E⟩ \lor x = ⟨C, F⟩) \land φ) \to (x \in T \land \exists a \exists b (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V)))$
94	93	ex	$⊢ (x = ⟨B, E⟩ \lor x = ⟨C, F⟩) \to (φ \to (x \in T \land \exists a \exists b (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V))))$
95	43 94	sylbi	$⊢ x \in \{⟨B, E⟩, ⟨C, F⟩\} \to (φ \to (x \in T \land \exists a \exists b (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V))))$
96	95	com12	$⊢ φ \to (x \in \{⟨B, E⟩, ⟨C, F⟩\} \to (x \in T \land \exists a \exists b (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V))))$
97	48 96	impbid	$⊢ φ \to ((x \in T \land \exists a \exists b (x = ⟨a, b⟩ \land (a \in (V ∖ \{A\}) \land b \in V))) \leftrightarrow x \in \{⟨B, E⟩, ⟨C, F⟩\})$
98	11 97	bitrid	$⊢ φ \to ((x \in T \land x \in ((V ∖ \{A\}) \times V)) \leftrightarrow x \in \{⟨B, E⟩, ⟨C, F⟩\})$
99	9 98	bitrid	$⊢ φ \to (x \in (T \cap ((V ∖ \{A\}) \times V)) \leftrightarrow x \in \{⟨B, E⟩, ⟨C, F⟩\})$
100	99	eqrdv	$⊢ φ \to T \cap ((V ∖ \{A\}) \times V) = \{⟨B, E⟩, ⟨C, F⟩\}$
101	8 100	eqtrid	$⊢ φ \to {T ↾}_{(V ∖ \{A\})} = \{⟨B, E⟩, ⟨C, F⟩\}$

Metamath Proof Explorer

Theorem tpres

Proof