wemaplem2

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$
	wemaplem2.px1	$⊢ φ \to a \in A$
	wemaplem2.px2	$⊢ φ \to P (a) S X (a)$
	wemaplem2.px3	$⊢ φ \to \forall c \in A (c R a \to P (c) = X (c))$
	wemaplem2.xq1	$⊢ φ \to b \in A$
	wemaplem2.xq2	$⊢ φ \to X (b) S Q (b)$
	wemaplem2.xq3	$⊢ φ \to \forall c \in A (c R b \to X (c) = Q (c))$
Assertion	wemaplem2	$⊢ φ \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		wemaplem2.px1	$⊢ φ \to a \in A$
8		wemaplem2.px2	$⊢ φ \to P (a) S X (a)$
9		wemaplem2.px3	$⊢ φ \to \forall c \in A (c R a \to P (c) = X (c))$
10		wemaplem2.xq1	$⊢ φ \to b \in A$
11		wemaplem2.xq2	$⊢ φ \to X (b) S Q (b)$
12		wemaplem2.xq3	$⊢ φ \to \forall c \in A (c R b \to X (c) = Q (c))$
13	7 10	ifcld	$⊢ φ \to if (a R b, a, b) \in A$
14	8	adantr	$⊢ (φ \land a R b) \to P (a) S X (a)$
15		breq1	$⊢ c = a \to (c R b \leftrightarrow a R b)$
16		fveq2	$⊢ c = a \to X (c) = X (a)$
17		fveq2	$⊢ c = a \to Q (c) = Q (a)$
18	16 17	eqeq12d	$⊢ c = a \to (X (c) = Q (c) \leftrightarrow X (a) = Q (a))$
19	15 18	imbi12d	$⊢ c = a \to ((c R b \to X (c) = Q (c)) \leftrightarrow (a R b \to X (a) = Q (a)))$
20	19 12 7	rspcdva	$⊢ φ \to (a R b \to X (a) = Q (a))$
21	20	imp	$⊢ (φ \land a R b) \to X (a) = Q (a)$
22	14 21	breqtrd	$⊢ (φ \land a R b) \to P (a) S Q (a)$
23		iftrue	$⊢ a R b \to if (a R b, a, b) = a$
24	23	fveq2d	$⊢ a R b \to P (if (a R b, a, b)) = P (a)$
25	23	fveq2d	$⊢ a R b \to Q (if (a R b, a, b)) = Q (a)$
26	24 25	breq12d	$⊢ a R b \to (P (if (a R b, a, b)) S Q (if (a R b, a, b)) \leftrightarrow P (a) S Q (a))$
27	26	adantl	$⊢ (φ \land a R b) \to (P (if (a R b, a, b)) S Q (if (a R b, a, b)) \leftrightarrow P (a) S Q (a))$
28	22 27	mpbird	$⊢ (φ \land a R b) \to P (if (a R b, a, b)) S Q (if (a R b, a, b))$
29	6	adantr	$⊢ (φ \land a = b) \to S Po B$
30		elmapi	$⊢ P \in (B^{A}) \to P : A ⟶ B$
31	2 30	syl	$⊢ φ \to P : A ⟶ B$
32	31 10	ffvelrnd	$⊢ φ \to P (b) \in B$
33		elmapi	$⊢ X \in (B^{A}) \to X : A ⟶ B$
34	3 33	syl	$⊢ φ \to X : A ⟶ B$
35	34 10	ffvelrnd	$⊢ φ \to X (b) \in B$
36		elmapi	$⊢ Q \in (B^{A}) \to Q : A ⟶ B$
37	4 36	syl	$⊢ φ \to Q : A ⟶ B$
38	37 10	ffvelrnd	$⊢ φ \to Q (b) \in B$
39	32 35 38	3jca	$⊢ φ \to (P (b) \in B \land X (b) \in B \land Q (b) \in B)$
40	39	adantr	$⊢ (φ \land a = b) \to (P (b) \in B \land X (b) \in B \land Q (b) \in B)$
41		fveq2	$⊢ a = b \to P (a) = P (b)$
42		fveq2	$⊢ a = b \to X (a) = X (b)$
43	41 42	breq12d	$⊢ a = b \to (P (a) S X (a) \leftrightarrow P (b) S X (b))$
44	8 43	syl5ibcom	$⊢ φ \to (a = b \to P (b) S X (b))$
45	44	imp	$⊢ (φ \land a = b) \to P (b) S X (b)$
46	11	adantr	$⊢ (φ \land a = b) \to X (b) S Q (b)$
47		potr	$⊢ (S Po B \land (P (b) \in B \land X (b) \in B \land Q (b) \in B)) \to ((P (b) S X (b) \land X (b) S Q (b)) \to P (b) S Q (b))$
48	47	imp	$⊢ ((S Po B \land (P (b) \in B \land X (b) \in B \land Q (b) \in B)) \land (P (b) S X (b) \land X (b) S Q (b))) \to P (b) S Q (b)$
49	29 40 45 46 48	syl22anc	$⊢ (φ \land a = b) \to P (b) S Q (b)$
50		ifeq1	$⊢ a = b \to if (a R b, a, b) = if (a R b, b, b)$
51		ifid	$⊢ if (a R b, b, b) = b$
52	50 51	eqtrdi	$⊢ a = b \to if (a R b, a, b) = b$
53	52	fveq2d	$⊢ a = b \to P (if (a R b, a, b)) = P (b)$
54	52	fveq2d	$⊢ a = b \to Q (if (a R b, a, b)) = Q (b)$
55	53 54	breq12d	$⊢ a = b \to (P (if (a R b, a, b)) S Q (if (a R b, a, b)) \leftrightarrow P (b) S Q (b))$
56	55	adantl	$⊢ (φ \land a = b) \to (P (if (a R b, a, b)) S Q (if (a R b, a, b)) \leftrightarrow P (b) S Q (b))$
57	49 56	mpbird	$⊢ (φ \land a = b) \to P (if (a R b, a, b)) S Q (if (a R b, a, b))$
58		breq1	$⊢ c = b \to (c R a \leftrightarrow b R a)$
59		fveq2	$⊢ c = b \to P (c) = P (b)$
60		fveq2	$⊢ c = b \to X (c) = X (b)$
61	59 60	eqeq12d	$⊢ c = b \to (P (c) = X (c) \leftrightarrow P (b) = X (b))$
62	58 61	imbi12d	$⊢ c = b \to ((c R a \to P (c) = X (c)) \leftrightarrow (b R a \to P (b) = X (b)))$
63	62 9 10	rspcdva	$⊢ φ \to (b R a \to P (b) = X (b))$
64	63	imp	$⊢ (φ \land b R a) \to P (b) = X (b)$
65	11	adantr	$⊢ (φ \land b R a) \to X (b) S Q (b)$
66	64 65	eqbrtrd	$⊢ (φ \land b R a) \to P (b) S Q (b)$
67		sopo	$⊢ R Or A \to R Po A$
68	5 67	syl	$⊢ φ \to R Po A$
69		po2nr	$⊢ (R Po A \land (b \in A \land a \in A)) \to \neg (b R a \land a R b)$
70	68 10 7 69	syl12anc	$⊢ φ \to \neg (b R a \land a R b)$
71		nan	$⊢ (φ \to \neg (b R a \land a R b)) \leftrightarrow ((φ \land b R a) \to \neg a R b)$
72	70 71	mpbi	$⊢ (φ \land b R a) \to \neg a R b$
73		iffalse	$⊢ \neg a R b \to if (a R b, a, b) = b$
74	73	fveq2d	$⊢ \neg a R b \to P (if (a R b, a, b)) = P (b)$
75	73	fveq2d	$⊢ \neg a R b \to Q (if (a R b, a, b)) = Q (b)$
76	74 75	breq12d	$⊢ \neg a R b \to (P (if (a R b, a, b)) S Q (if (a R b, a, b)) \leftrightarrow P (b) S Q (b))$
77	72 76	syl	$⊢ (φ \land b R a) \to (P (if (a R b, a, b)) S Q (if (a R b, a, b)) \leftrightarrow P (b) S Q (b))$
78	66 77	mpbird	$⊢ (φ \land b R a) \to P (if (a R b, a, b)) S Q (if (a R b, a, b))$
79		solin	$⊢ (R Or A \land (a \in A \land b \in A)) \to (a R b \lor a = b \lor b R a)$
80	5 7 10 79	syl12anc	$⊢ φ \to (a R b \lor a = b \lor b R a)$
81	28 57 78 80	mpjao3dan	$⊢ φ \to P (if (a R b, a, b)) S Q (if (a R b, a, b))$
82		r19.26	$⊢ \forall c \in A ((c R a \to P (c) = X (c)) \land (c R b \to X (c) = Q (c))) \leftrightarrow (\forall c \in A (c R a \to P (c) = X (c)) \land \forall c \in A (c R b \to X (c) = Q (c)))$
83	9 12 82	sylanbrc	$⊢ φ \to \forall c \in A ((c R a \to P (c) = X (c)) \land (c R b \to X (c) = Q (c)))$
84	5 7 10	3jca	$⊢ φ \to (R Or A \land a \in A \land b \in A)$
85		anim12	$⊢ ((c R a \to P (c) = X (c)) \land (c R b \to X (c) = Q (c))) \to ((c R a \land c R b) \to (P (c) = X (c) \land X (c) = Q (c)))$
86		eqtr	$⊢ (P (c) = X (c) \land X (c) = Q (c)) \to P (c) = Q (c)$
87	85 86	syl6	$⊢ ((c R a \to P (c) = X (c)) \land (c R b \to X (c) = Q (c))) \to ((c R a \land c R b) \to P (c) = Q (c))$
88	87	ralimi	$⊢ \forall c \in A ((c R a \to P (c) = X (c)) \land (c R b \to X (c) = Q (c))) \to \forall c \in A ((c R a \land c R b) \to P (c) = Q (c))$
89		simpl1	$⊢ ((R Or A \land a \in A \land b \in A) \land c \in A) \to R Or A$
90		simpr	$⊢ ((R Or A \land a \in A \land b \in A) \land c \in A) \to c \in A$
91		simpl2	$⊢ ((R Or A \land a \in A \land b \in A) \land c \in A) \to a \in A$
92		simpl3	$⊢ ((R Or A \land a \in A \land b \in A) \land c \in A) \to b \in A$
93		soltmin	$⊢ (R Or A \land (c \in A \land a \in A \land b \in A)) \to (c R if (a R b, a, b) \leftrightarrow (c R a \land c R b))$
94	89 90 91 92 93	syl13anc	$⊢ ((R Or A \land a \in A \land b \in A) \land c \in A) \to (c R if (a R b, a, b) \leftrightarrow (c R a \land c R b))$
95	94	biimpd	$⊢ ((R Or A \land a \in A \land b \in A) \land c \in A) \to (c R if (a R b, a, b) \to (c R a \land c R b))$
96	95	imim1d	$⊢ ((R Or A \land a \in A \land b \in A) \land c \in A) \to (((c R a \land c R b) \to P (c) = Q (c)) \to (c R if (a R b, a, b) \to P (c) = Q (c)))$
97	96	ralimdva	$⊢ (R Or A \land a \in A \land b \in A) \to (\forall c \in A ((c R a \land c R b) \to P (c) = Q (c)) \to \forall c \in A (c R if (a R b, a, b) \to P (c) = Q (c)))$
98	84 88 97	syl2im	$⊢ φ \to (\forall c \in A ((c R a \to P (c) = X (c)) \land (c R b \to X (c) = Q (c))) \to \forall c \in A (c R if (a R b, a, b) \to P (c) = Q (c)))$
99	83 98	mpd	$⊢ φ \to \forall c \in A (c R if (a R b, a, b) \to P (c) = Q (c))$
100		fveq2	$⊢ d = if (a R b, a, b) \to P (d) = P (if (a R b, a, b))$
101		fveq2	$⊢ d = if (a R b, a, b) \to Q (d) = Q (if (a R b, a, b))$
102	100 101	breq12d	$⊢ d = if (a R b, a, b) \to (P (d) S Q (d) \leftrightarrow P (if (a R b, a, b)) S Q (if (a R b, a, b)))$
103		breq2	$⊢ d = if (a R b, a, b) \to (c R d \leftrightarrow c R if (a R b, a, b))$
104	103	imbi1d	$⊢ d = if (a R b, a, b) \to ((c R d \to P (c) = Q (c)) \leftrightarrow (c R if (a R b, a, b) \to P (c) = Q (c)))$
105	104	ralbidv	$⊢ d = if (a R b, a, b) \to (\forall c \in A (c R d \to P (c) = Q (c)) \leftrightarrow \forall c \in A (c R if (a R b, a, b) \to P (c) = Q (c)))$
106	102 105	anbi12d	$⊢ d = if (a R b, a, b) \to ((P (d) S Q (d) \land \forall c \in A (c R d \to P (c) = Q (c))) \leftrightarrow (P (if (a R b, a, b)) S Q (if (a R b, a, b)) \land \forall c \in A (c R if (a R b, a, b) \to P (c) = Q (c))))$
107	106	rspcev	$⊢ (if (a R b, a, b) \in A \land (P (if (a R b, a, b)) S Q (if (a R b, a, b)) \land \forall c \in A (c R if (a R b, a, b) \to P (c) = Q (c)))) \to \exists d \in A (P (d) S Q (d) \land \forall c \in A (c R d \to P (c) = Q (c)))$
108	13 81 99 107	syl12anc	$⊢ φ \to \exists d \in A (P (d) S Q (d) \land \forall c \in A (c R d \to P (c) = Q (c)))$
109	1	wemaplem1	$⊢ (P \in (B^{A}) \land Q \in (B^{A})) \to (P T Q \leftrightarrow \exists d \in A (P (d) S Q (d) \land \forall c \in A (c R d \to P (c) = Q (c))))$
110	2 4 109	syl2anc	$⊢ φ \to (P T Q \leftrightarrow \exists d \in A (P (d) S Q (d) \land \forall c \in A (c R d \to P (c) = Q (c))))$
111	108 110	mpbird	$⊢ φ \to P T Q$

Metamath Proof Explorer

Theorem wemaplem2

Proof