wemaplem3

Description: Lemma for wemapso . Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015) (Revised by AV, 21-Jul-2024)

	Ref	Expression
Hypotheses	wemapso.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in A (x (z) S y (z) \land \forall w \in A (w R z \to x (w) = y (w)))\}$
	wemaplem2.p	$⊢ φ \to P \in (B^{A})$
	wemaplem2.x	$⊢ φ \to X \in (B^{A})$
	wemaplem2.q	$⊢ φ \to Q \in (B^{A})$
	wemaplem2.r	$⊢ φ \to R Or A$
	wemaplem2.s	$⊢ φ \to S Po B$
	wemaplem3.px	$⊢ φ \to P T X$
	wemaplem3.xq	$⊢ φ \to X T Q$
Assertion	wemaplem3	$⊢ φ \to P T Q$

Proof

Step	Hyp	Ref	Expression
1		wemapso.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in A (x (z) S y (z) \land \forall w \in A (w R z \to x (w) = y (w)))\}$
2		wemaplem2.p	$⊢ φ \to P \in (B^{A})$
3		wemaplem2.x	$⊢ φ \to X \in (B^{A})$
4		wemaplem2.q	$⊢ φ \to Q \in (B^{A})$
5		wemaplem2.r	$⊢ φ \to R Or A$
6		wemaplem2.s	$⊢ φ \to S Po B$
7		wemaplem3.px	$⊢ φ \to P T X$
8		wemaplem3.xq	$⊢ φ \to X T Q$
9	1	wemaplem1	$⊢ (P \in (B^{A}) \land X \in (B^{A})) \to (P T X \leftrightarrow \exists a \in A (P (a) S X (a) \land \forall c \in A (c R a \to P (c) = X (c))))$
10	2 3 9	syl2anc	$⊢ φ \to (P T X \leftrightarrow \exists a \in A (P (a) S X (a) \land \forall c \in A (c R a \to P (c) = X (c))))$
11	7 10	mpbid	$⊢ φ \to \exists a \in A (P (a) S X (a) \land \forall c \in A (c R a \to P (c) = X (c)))$
12	1	wemaplem1	$⊢ (X \in (B^{A}) \land Q \in (B^{A})) \to (X T Q \leftrightarrow \exists b \in A (X (b) S Q (b) \land \forall c \in A (c R b \to X (c) = Q (c))))$
13	3 4 12	syl2anc	$⊢ φ \to (X T Q \leftrightarrow \exists b \in A (X (b) S Q (b) \land \forall c \in A (c R b \to X (c) = Q (c))))$
14	8 13	mpbid	$⊢ φ \to \exists b \in A (X (b) S Q (b) \land \forall c \in A (c R b \to X (c) = Q (c)))$
15	2	ad2antrr	$⊢ ((φ \land (a \in A \land (P (a) S X (a) \land \forall c \in A (c R a \to P (c) = X (c))))) \land (b \in A \land (X (b) S Q (b) \land \forall c \in A (c R b \to X (c) = Q (c))))) \to P \in (B^{A})$
16	3	ad2antrr	$⊢ ((φ \land (a \in A \land (P (a) S X (a) \land \forall c \in A (c R a \to P (c) = X (c))))) \land (b \in A \land (X (b) S Q (b) \land \forall c \in A (c R b \to X (c) = Q (c))))) \to X \in (B^{A})$
17	4	ad2antrr	$⊢ ((φ \land (a \in A \land (P (a) S X (a) \land \forall c \in A (c R a \to P (c) = X (c))))) \land (b \in A \land (X (b) S Q (b) \land \forall c \in A (c R b \to X (c) = Q (c))))) \to Q \in (B^{A})$
18	5	ad2antrr	$⊢ ((φ \land (a \in A \land (P (a) S X (a) \land \forall c \in A (c R a \to P (c) = X (c))))) \land (b \in A \land (X (b) S Q (b) \land \forall c \in A (c R b \to X (c) = Q (c))))) \to R Or A$
19	6	ad2antrr	$⊢ ((φ \land (a \in A \land (P (a) S X (a) \land \forall c \in A (c R a \to P (c) = X (c))))) \land (b \in A \land (X (b) S Q (b) \land \forall c \in A (c R b \to X (c) = Q (c))))) \to S Po B$
20		simplrl	$⊢ ((φ \land (a \in A \land (P (a) S X (a) \land \forall c \in A (c R a \to P (c) = X (c))))) \land (b \in A \land (X (b) S Q (b) \land \forall c \in A (c R b \to X (c) = Q (c))))) \to a \in A$
21		simp2rl	$⊢ (φ \land (a \in A \land (P (a) S X (a) \land \forall c \in A (c R a \to P (c) = X (c)))) \land (b \in A \land (X (b) S Q (b) \land \forall c \in A (c R b \to X (c) = Q (c))))) \to P (a) S X (a)$
22	21	3expa	$⊢ ((φ \land (a \in A \land (P (a) S X (a) \land \forall c \in A (c R a \to P (c) = X (c))))) \land (b \in A \land (X (b) S Q (b) \land \forall c \in A (c R b \to X (c) = Q (c))))) \to P (a) S X (a)$
23		simprr	$⊢ (a \in A \land (P (a) S X (a) \land \forall c \in A (c R a \to P (c) = X (c)))) \to \forall c \in A (c R a \to P (c) = X (c))$
24	23	ad2antlr	$⊢ ((φ \land (a \in A \land (P (a) S X (a) \land \forall c \in A (c R a \to P (c) = X (c))))) \land (b \in A \land (X (b) S Q (b) \land \forall c \in A (c R b \to X (c) = Q (c))))) \to \forall c \in A (c R a \to P (c) = X (c))$
25		simprl	$⊢ ((φ \land (a \in A \land (P (a) S X (a) \land \forall c \in A (c R a \to P (c) = X (c))))) \land (b \in A \land (X (b) S Q (b) \land \forall c \in A (c R b \to X (c) = Q (c))))) \to b \in A$
26		simprrl	$⊢ ((φ \land (a \in A \land (P (a) S X (a) \land \forall c \in A (c R a \to P (c) = X (c))))) \land (b \in A \land (X (b) S Q (b) \land \forall c \in A (c R b \to X (c) = Q (c))))) \to X (b) S Q (b)$
27		simprrr	$⊢ ((φ \land (a \in A \land (P (a) S X (a) \land \forall c \in A (c R a \to P (c) = X (c))))) \land (b \in A \land (X (b) S Q (b) \land \forall c \in A (c R b \to X (c) = Q (c))))) \to \forall c \in A (c R b \to X (c) = Q (c))$
28	1 15 16 17 18 19 20 22 24 25 26 27	wemaplem2	$⊢ ((φ \land (a \in A \land (P (a) S X (a) \land \forall c \in A (c R a \to P (c) = X (c))))) \land (b \in A \land (X (b) S Q (b) \land \forall c \in A (c R b \to X (c) = Q (c))))) \to P T Q$
29	28	rexlimdvaa	$⊢ (φ \land (a \in A \land (P (a) S X (a) \land \forall c \in A (c R a \to P (c) = X (c))))) \to (\exists b \in A (X (b) S Q (b) \land \forall c \in A (c R b \to X (c) = Q (c))) \to P T Q)$
30	29	rexlimdvaa	$⊢ φ \to (\exists a \in A (P (a) S X (a) \land \forall c \in A (c R a \to P (c) = X (c))) \to (\exists b \in A (X (b) S Q (b) \land \forall c \in A (c R b \to X (c) = Q (c))) \to P T Q))$
31	11 14 30	mp2d	$⊢ φ \to P T Q$

Metamath Proof Explorer

Theorem wemaplem3

Proof