bropfvvvv

Description: If a binary relation holds for the result of an operation which is a function value, the involved classes are sets. (Contributed by AV, 31-Dec-2020) (Revised by AV, 16-Jan-2021)

	Ref	Expression
Hypotheses	bropfvvvv.o	$⊢ O = (a \in U ⟼ (b \in V, c \in W ⟼ \{⟨d, e⟩ \| φ\}))$
	bropfvvvv.oo	$⊢ (A \in U \land B \in S \land C \in T) \to B O (A) C = \{⟨d, e⟩ \| θ\}$
	bropfvvvv.s	$⊢ a = A \to V = S$
	bropfvvvv.t	$⊢ a = A \to W = T$
	bropfvvvv.p	$⊢ a = A \to (φ \leftrightarrow ψ)$
Assertion	bropfvvvv	$⊢ (S \in X \land T \in Y) \to (D (B O (A) C) E \to (A \in U \land (B \in S \land C \in T) \land (D \in V \land E \in V)))$

Proof

Step	Hyp	Ref	Expression
1		bropfvvvv.o	$⊢ O = (a \in U ⟼ (b \in V, c \in W ⟼ \{⟨d, e⟩ \| φ\}))$
2		bropfvvvv.oo	$⊢ (A \in U \land B \in S \land C \in T) \to B O (A) C = \{⟨d, e⟩ \| θ\}$
3		bropfvvvv.s	$⊢ a = A \to V = S$
4		bropfvvvv.t	$⊢ a = A \to W = T$
5		bropfvvvv.p	$⊢ a = A \to (φ \leftrightarrow ψ)$
6		brovpreldm	$⊢ D (B O (A) C) E \to ⟨B, C⟩ \in dom O (A)$
7	5	opabbidv	$⊢ a = A \to \{⟨d, e⟩ \| φ\} = \{⟨d, e⟩ \| ψ\}$
8	3 4 7	mpoeq123dv	$⊢ a = A \to (b \in V, c \in W ⟼ \{⟨d, e⟩ \| φ\}) = (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\})$
9	8 1	fvmptg	$⊢ (A \in U \land (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\}) \in V) \to O (A) = (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\})$
10	9	dmeqd	$⊢ (A \in U \land (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\}) \in V) \to dom O (A) = dom (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\})$
11	10	eleq2d	$⊢ (A \in U \land (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\}) \in V) \to (⟨B, C⟩ \in dom O (A) \leftrightarrow ⟨B, C⟩ \in dom (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\}))$
12		dmoprabss	$⊢ dom \{⟨⟨b, c⟩, z⟩ \| ((b \in S \land c \in T) \land z = \{⟨d, e⟩ \| ψ\})\} \subseteq S \times T$
13	12	sseli	$⊢ ⟨B, C⟩ \in dom \{⟨⟨b, c⟩, z⟩ \| ((b \in S \land c \in T) \land z = \{⟨d, e⟩ \| ψ\})\} \to ⟨B, C⟩ \in (S \times T)$
14	1 2	bropfvvvvlem	$⊢ (⟨B, C⟩ \in (S \times T) \land D (B O (A) C) E) \to (A \in U \land (B \in S \land C \in T) \land (D \in V \land E \in V))$
15	14	ex	$⊢ ⟨B, C⟩ \in (S \times T) \to (D (B O (A) C) E \to (A \in U \land (B \in S \land C \in T) \land (D \in V \land E \in V)))$
16	13 15	syl	$⊢ ⟨B, C⟩ \in dom \{⟨⟨b, c⟩, z⟩ \| ((b \in S \land c \in T) \land z = \{⟨d, e⟩ \| ψ\})\} \to (D (B O (A) C) E \to (A \in U \land (B \in S \land C \in T) \land (D \in V \land E \in V)))$
17		df-mpo	$⊢ (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\}) = \{⟨⟨b, c⟩, z⟩ \| ((b \in S \land c \in T) \land z = \{⟨d, e⟩ \| ψ\})\}$
18	17	dmeqi	$⊢ dom (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\}) = dom \{⟨⟨b, c⟩, z⟩ \| ((b \in S \land c \in T) \land z = \{⟨d, e⟩ \| ψ\})\}$
19	16 18	eleq2s	$⊢ ⟨B, C⟩ \in dom (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\}) \to (D (B O (A) C) E \to (A \in U \land (B \in S \land C \in T) \land (D \in V \land E \in V)))$
20	11 19	syl6bi	$⊢ (A \in U \land (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\}) \in V) \to (⟨B, C⟩ \in dom O (A) \to (D (B O (A) C) E \to (A \in U \land (B \in S \land C \in T) \land (D \in V \land E \in V))))$
21	20	com23	$⊢ (A \in U \land (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\}) \in V) \to (D (B O (A) C) E \to (⟨B, C⟩ \in dom O (A) \to (A \in U \land (B \in S \land C \in T) \land (D \in V \land E \in V))))$
22	21	a1d	$⊢ (A \in U \land (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\}) \in V) \to ((S \in X \land T \in Y) \to (D (B O (A) C) E \to (⟨B, C⟩ \in dom O (A) \to (A \in U \land (B \in S \land C \in T) \land (D \in V \land E \in V)))))$
23		ianor	$⊢ \neg (A \in U \land (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\}) \in V) \leftrightarrow (\neg A \in U \lor \neg (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\}) \in V)$
24	1	fvmptndm	$⊢ \neg A \in U \to O (A) = \emptyset$
25	24	dmeqd	$⊢ \neg A \in U \to dom O (A) = dom \emptyset$
26	25	eleq2d	$⊢ \neg A \in U \to (⟨B, C⟩ \in dom O (A) \leftrightarrow ⟨B, C⟩ \in dom \emptyset)$
27		dm0	$⊢ dom \emptyset = \emptyset$
28	27	eleq2i	$⊢ ⟨B, C⟩ \in dom \emptyset \leftrightarrow ⟨B, C⟩ \in \emptyset$
29	26 28	syl6bb	$⊢ \neg A \in U \to (⟨B, C⟩ \in dom O (A) \leftrightarrow ⟨B, C⟩ \in \emptyset)$
30		noel	$⊢ \neg ⟨B, C⟩ \in \emptyset$
31	30	pm2.21i	$⊢ ⟨B, C⟩ \in \emptyset \to (D (B O (A) C) E \to (A \in U \land (B \in S \land C \in T) \land (D \in V \land E \in V)))$
32	29 31	syl6bi	$⊢ \neg A \in U \to (⟨B, C⟩ \in dom O (A) \to (D (B O (A) C) E \to (A \in U \land (B \in S \land C \in T) \land (D \in V \land E \in V))))$
33	32	a1d	$⊢ \neg A \in U \to ((S \in X \land T \in Y) \to (⟨B, C⟩ \in dom O (A) \to (D (B O (A) C) E \to (A \in U \land (B \in S \land C \in T) \land (D \in V \land E \in V)))))$
34		notnotb	$⊢ A \in U \leftrightarrow \neg \neg A \in U$
35		elex	$⊢ S \in X \to S \in V$
36		elex	$⊢ T \in Y \to T \in V$
37	35 36	anim12i	$⊢ (S \in X \land T \in Y) \to (S \in V \land T \in V)$
38	37	adantl	$⊢ (A \in U \land (S \in X \land T \in Y)) \to (S \in V \land T \in V)$
39		mpoexga	$⊢ (S \in V \land T \in V) \to (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\}) \in V$
40	38 39	syl	$⊢ (A \in U \land (S \in X \land T \in Y)) \to (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\}) \in V$
41	40	pm2.24d	$⊢ (A \in U \land (S \in X \land T \in Y)) \to (\neg (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\}) \in V \to (⟨B, C⟩ \in dom O (A) \to (D (B O (A) C) E \to (A \in U \land (B \in S \land C \in T) \land (D \in V \land E \in V)))))$
42	41	ex	$⊢ A \in U \to ((S \in X \land T \in Y) \to (\neg (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\}) \in V \to (⟨B, C⟩ \in dom O (A) \to (D (B O (A) C) E \to (A \in U \land (B \in S \land C \in T) \land (D \in V \land E \in V))))))$
43	42	com23	$⊢ A \in U \to (\neg (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\}) \in V \to ((S \in X \land T \in Y) \to (⟨B, C⟩ \in dom O (A) \to (D (B O (A) C) E \to (A \in U \land (B \in S \land C \in T) \land (D \in V \land E \in V))))))$
44	34 43	sylbir	$⊢ \neg \neg A \in U \to (\neg (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\}) \in V \to ((S \in X \land T \in Y) \to (⟨B, C⟩ \in dom O (A) \to (D (B O (A) C) E \to (A \in U \land (B \in S \land C \in T) \land (D \in V \land E \in V))))))$
45	44	imp	$⊢ (\neg \neg A \in U \land \neg (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\}) \in V) \to ((S \in X \land T \in Y) \to (⟨B, C⟩ \in dom O (A) \to (D (B O (A) C) E \to (A \in U \land (B \in S \land C \in T) \land (D \in V \land E \in V)))))$
46	33 45	jaoi3	$⊢ (\neg A \in U \lor \neg (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\}) \in V) \to ((S \in X \land T \in Y) \to (⟨B, C⟩ \in dom O (A) \to (D (B O (A) C) E \to (A \in U \land (B \in S \land C \in T) \land (D \in V \land E \in V)))))$
47	23 46	sylbi	$⊢ \neg (A \in U \land (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\}) \in V) \to ((S \in X \land T \in Y) \to (⟨B, C⟩ \in dom O (A) \to (D (B O (A) C) E \to (A \in U \land (B \in S \land C \in T) \land (D \in V \land E \in V)))))$
48	47	com34	$⊢ \neg (A \in U \land (b \in S, c \in T ⟼ \{⟨d, e⟩ \| ψ\}) \in V) \to ((S \in X \land T \in Y) \to (D (B O (A) C) E \to (⟨B, C⟩ \in dom O (A) \to (A \in U \land (B \in S \land C \in T) \land (D \in V \land E \in V)))))$
49	22 48	pm2.61i	$⊢ (S \in X \land T \in Y) \to (D (B O (A) C) E \to (⟨B, C⟩ \in dom O (A) \to (A \in U \land (B \in S \land C \in T) \land (D \in V \land E \in V))))$
50	6 49	mpdi	$⊢ (S \in X \land T \in Y) \to (D (B O (A) C) E \to (A \in U \land (B \in S \land C \in T) \land (D \in V \land E \in V)))$

Metamath Proof Explorer

Theorem bropfvvvv

Proof