bropfvvvvlem

Description: Lemma for bropfvvvv . (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⟩ \| θ\}$
Assertion	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))$

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		opelxp	$⊢ ⟨B, C⟩ \in (S \times T) \leftrightarrow (B \in S \land C \in T)$
4		brne0	$⊢ D (B O (A) C) E \to B O (A) C \neq \emptyset$
5	2	3expb	$⊢ (A \in U \land (B \in S \land C \in T)) \to B O (A) C = \{⟨d, e⟩ \| θ\}$
6	5	breqd	$⊢ (A \in U \land (B \in S \land C \in T)) \to (D (B O (A) C) E \leftrightarrow D \{⟨d, e⟩ \| θ\} E)$
7		brabv	$⊢ D \{⟨d, e⟩ \| θ\} E \to (D \in V \land E \in V)$
8	7	anim2i	$⊢ (A \in U \land D \{⟨d, e⟩ \| θ\} E) \to (A \in U \land (D \in V \land E \in V))$
9	8	ex	$⊢ A \in U \to (D \{⟨d, e⟩ \| θ\} E \to (A \in U \land (D \in V \land E \in V)))$
10	9	adantr	$⊢ (A \in U \land (B \in S \land C \in T)) \to (D \{⟨d, e⟩ \| θ\} E \to (A \in U \land (D \in V \land E \in V)))$
11	6 10	sylbid	$⊢ (A \in U \land (B \in S \land C \in T)) \to (D (B O (A) C) E \to (A \in U \land (D \in V \land E \in V)))$
12	11	ex	$⊢ A \in U \to ((B \in S \land C \in T) \to (D (B O (A) C) E \to (A \in U \land (D \in V \land E \in V))))$
13	12	com23	$⊢ A \in U \to (D (B O (A) C) E \to ((B \in S \land C \in T) \to (A \in U \land (D \in V \land E \in V))))$
14	13	a1d	$⊢ A \in U \to (B O (A) C \neq \emptyset \to (D (B O (A) C) E \to ((B \in S \land C \in T) \to (A \in U \land (D \in V \land E \in V)))))$
15	1	fvmptndm	$⊢ \neg A \in U \to O (A) = \emptyset$
16		df-ov	$⊢ B O (A) C = O (A) (⟨B, C⟩)$
17		fveq1	$⊢ O (A) = \emptyset \to O (A) (⟨B, C⟩) = \emptyset (⟨B, C⟩)$
18	16 17	syl5eq	$⊢ O (A) = \emptyset \to B O (A) C = \emptyset (⟨B, C⟩)$
19		0fv	$⊢ \emptyset (⟨B, C⟩) = \emptyset$
20	18 19	eqtrdi	$⊢ O (A) = \emptyset \to B O (A) C = \emptyset$
21		eqneqall	$⊢ B O (A) C = \emptyset \to (B O (A) C \neq \emptyset \to (D (B O (A) C) E \to ((B \in S \land C \in T) \to (A \in U \land (D \in V \land E \in V)))))$
22	15 20 21	3syl	$⊢ \neg A \in U \to (B O (A) C \neq \emptyset \to (D (B O (A) C) E \to ((B \in S \land C \in T) \to (A \in U \land (D \in V \land E \in V)))))$
23	14 22	pm2.61i	$⊢ B O (A) C \neq \emptyset \to (D (B O (A) C) E \to ((B \in S \land C \in T) \to (A \in U \land (D \in V \land E \in V))))$
24	4 23	mpcom	$⊢ D (B O (A) C) E \to ((B \in S \land C \in T) \to (A \in U \land (D \in V \land E \in V)))$
25	24	com12	$⊢ (B \in S \land C \in T) \to (D (B O (A) C) E \to (A \in U \land (D \in V \land E \in V)))$
26	25	anc2ri	$⊢ (B \in S \land C \in T) \to (D (B O (A) C) E \to ((A \in U \land (D \in V \land E \in V)) \land (B \in S \land C \in T)))$
27		3anan32	$⊢ (A \in U \land (B \in S \land C \in T) \land (D \in V \land E \in V)) \leftrightarrow ((A \in U \land (D \in V \land E \in V)) \land (B \in S \land C \in T))$
28	26 27	syl6ibr	$⊢ (B \in S \land C \in 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)))$
29	3 28	sylbi	$⊢ ⟨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)))$
30	29	imp	$⊢ (⟨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))$

Metamath Proof Explorer

Theorem bropfvvvvlem

Proof