wemapsolem

Description: Lemma for wemapso . (Contributed by Stefan O'Rear, 18-Jan-2015) (Revised by Mario Carneiro, 8-Feb-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)))\}$
	wemapsolem.1	$⊢ U \subseteq B^{A}$
	wemapsolem.2	$⊢ φ \to R Or A$
	wemapsolem.3	$⊢ φ \to S Or B$
	wemapsolem.4	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to \exists c \in dom (a ∖ b) \forall d \in dom (a ∖ b) \neg d R c$
Assertion	wemapsolem	$⊢ φ \to T Or U$

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		wemapsolem.1	$⊢ U \subseteq B^{A}$
3		wemapsolem.2	$⊢ φ \to R Or A$
4		wemapsolem.3	$⊢ φ \to S Or B$
5		wemapsolem.4	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to \exists c \in dom (a ∖ b) \forall d \in dom (a ∖ b) \neg d R c$
6		sopo	$⊢ S Or B \to S Po B$
7	4 6	syl	$⊢ φ \to S Po B$
8	1	wemappo	$⊢ (R Or A \land S Po B) \to T Po (B^{A})$
9	3 7 8	syl2anc	$⊢ φ \to T Po (B^{A})$
10		poss	$⊢ U \subseteq B^{A} \to (T Po (B^{A}) \to T Po U)$
11	2 9 10	mpsyl	$⊢ φ \to T Po U$
12		df-ne	$⊢ a \neq b \leftrightarrow \neg a = b$
13		simprll	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to a \in U$
14	2 13	sselid	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to a \in (B^{A})$
15		elmapi	$⊢ a \in (B^{A}) \to a : A ⟶ B$
16	14 15	syl	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to a : A ⟶ B$
17	16	ffnd	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to a Fn A$
18		simprlr	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to b \in U$
19	2 18	sselid	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to b \in (B^{A})$
20		elmapi	$⊢ b \in (B^{A}) \to b : A ⟶ B$
21	19 20	syl	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to b : A ⟶ B$
22	21	ffnd	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to b Fn A$
23		fndmdif	$⊢ (a Fn A \land b Fn A) \to dom (a ∖ b) = \{x \in A \| a (x) \neq b (x)\}$
24	17 22 23	syl2anc	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to dom (a ∖ b) = \{x \in A \| a (x) \neq b (x)\}$
25	24	eleq2d	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to (c \in dom (a ∖ b) \leftrightarrow c \in \{x \in A \| a (x) \neq b (x)\})$
26		nesym	$⊢ a (x) \neq b (x) \leftrightarrow \neg b (x) = a (x)$
27		fveq2	$⊢ x = c \to b (x) = b (c)$
28		fveq2	$⊢ x = c \to a (x) = a (c)$
29	27 28	eqeq12d	$⊢ x = c \to (b (x) = a (x) \leftrightarrow b (c) = a (c))$
30	29	notbid	$⊢ x = c \to (\neg b (x) = a (x) \leftrightarrow \neg b (c) = a (c))$
31	26 30	bitrid	$⊢ x = c \to (a (x) \neq b (x) \leftrightarrow \neg b (c) = a (c))$
32	31	elrab	$⊢ c \in \{x \in A \| a (x) \neq b (x)\} \leftrightarrow (c \in A \land \neg b (c) = a (c))$
33	25 32	bitrdi	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to (c \in dom (a ∖ b) \leftrightarrow (c \in A \land \neg b (c) = a (c)))$
34	24	eleq2d	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to (d \in dom (a ∖ b) \leftrightarrow d \in \{x \in A \| a (x) \neq b (x)\})$
35		fveq2	$⊢ x = d \to b (x) = b (d)$
36		fveq2	$⊢ x = d \to a (x) = a (d)$
37	35 36	eqeq12d	$⊢ x = d \to (b (x) = a (x) \leftrightarrow b (d) = a (d))$
38	37	notbid	$⊢ x = d \to (\neg b (x) = a (x) \leftrightarrow \neg b (d) = a (d))$
39	26 38	bitrid	$⊢ x = d \to (a (x) \neq b (x) \leftrightarrow \neg b (d) = a (d))$
40	39	elrab	$⊢ d \in \{x \in A \| a (x) \neq b (x)\} \leftrightarrow (d \in A \land \neg b (d) = a (d))$
41	34 40	bitrdi	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to (d \in dom (a ∖ b) \leftrightarrow (d \in A \land \neg b (d) = a (d)))$
42	41	imbi1d	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to ((d \in dom (a ∖ b) \to \neg d R c) \leftrightarrow ((d \in A \land \neg b (d) = a (d)) \to \neg d R c))$
43		impexp	$⊢ ((d \in A \land \neg b (d) = a (d)) \to \neg d R c) \leftrightarrow (d \in A \to (\neg b (d) = a (d) \to \neg d R c))$
44		con34b	$⊢ (d R c \to b (d) = a (d)) \leftrightarrow (\neg b (d) = a (d) \to \neg d R c)$
45	44	imbi2i	$⊢ (d \in A \to (d R c \to b (d) = a (d))) \leftrightarrow (d \in A \to (\neg b (d) = a (d) \to \neg d R c))$
46	43 45	bitr4i	$⊢ ((d \in A \land \neg b (d) = a (d)) \to \neg d R c) \leftrightarrow (d \in A \to (d R c \to b (d) = a (d)))$
47	42 46	bitrdi	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to ((d \in dom (a ∖ b) \to \neg d R c) \leftrightarrow (d \in A \to (d R c \to b (d) = a (d))))$
48	47	ralbidv2	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to (\forall d \in dom (a ∖ b) \neg d R c \leftrightarrow \forall d \in A (d R c \to b (d) = a (d)))$
49	33 48	anbi12d	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to ((c \in dom (a ∖ b) \land \forall d \in dom (a ∖ b) \neg d R c) \leftrightarrow ((c \in A \land \neg b (c) = a (c)) \land \forall d \in A (d R c \to b (d) = a (d))))$
50		anass	$⊢ ((c \in A \land \neg b (c) = a (c)) \land \forall d \in A (d R c \to b (d) = a (d))) \leftrightarrow (c \in A \land (\neg b (c) = a (c) \land \forall d \in A (d R c \to b (d) = a (d))))$
51	49 50	bitrdi	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to ((c \in dom (a ∖ b) \land \forall d \in dom (a ∖ b) \neg d R c) \leftrightarrow (c \in A \land (\neg b (c) = a (c) \land \forall d \in A (d R c \to b (d) = a (d)))))$
52	51	rexbidv2	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to (\exists c \in dom (a ∖ b) \forall d \in dom (a ∖ b) \neg d R c \leftrightarrow \exists c \in A (\neg b (c) = a (c) \land \forall d \in A (d R c \to b (d) = a (d))))$
53	5 52	mpbid	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to \exists c \in A (\neg b (c) = a (c) \land \forall d \in A (d R c \to b (d) = a (d)))$
54	4	ad2antrr	$⊢ ((φ \land ((a \in U \land b \in U) \land a \neq b)) \land c \in A) \to S Or B$
55	21	ffvelcdmda	$⊢ ((φ \land ((a \in U \land b \in U) \land a \neq b)) \land c \in A) \to b (c) \in B$
56	16	ffvelcdmda	$⊢ ((φ \land ((a \in U \land b \in U) \land a \neq b)) \land c \in A) \to a (c) \in B$
57		sotrieq	$⊢ (S Or B \land (b (c) \in B \land a (c) \in B)) \to (b (c) = a (c) \leftrightarrow \neg (b (c) S a (c) \lor a (c) S b (c)))$
58	57	con2bid	$⊢ (S Or B \land (b (c) \in B \land a (c) \in B)) \to ((b (c) S a (c) \lor a (c) S b (c)) \leftrightarrow \neg b (c) = a (c))$
59	58	biimprd	$⊢ (S Or B \land (b (c) \in B \land a (c) \in B)) \to (\neg b (c) = a (c) \to (b (c) S a (c) \lor a (c) S b (c)))$
60	54 55 56 59	syl12anc	$⊢ ((φ \land ((a \in U \land b \in U) \land a \neq b)) \land c \in A) \to (\neg b (c) = a (c) \to (b (c) S a (c) \lor a (c) S b (c)))$
61	60	anim1d	$⊢ ((φ \land ((a \in U \land b \in U) \land a \neq b)) \land c \in A) \to ((\neg b (c) = a (c) \land \forall d \in A (d R c \to b (d) = a (d))) \to ((b (c) S a (c) \lor a (c) S b (c)) \land \forall d \in A (d R c \to b (d) = a (d))))$
62	61	reximdva	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to (\exists c \in A (\neg b (c) = a (c) \land \forall d \in A (d R c \to b (d) = a (d))) \to \exists c \in A ((b (c) S a (c) \lor a (c) S b (c)) \land \forall d \in A (d R c \to b (d) = a (d))))$
63	53 62	mpd	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to \exists c \in A ((b (c) S a (c) \lor a (c) S b (c)) \land \forall d \in A (d R c \to b (d) = a (d)))$
64	1	wemaplem1	$⊢ (b \in V \land a \in V) \to (b T a \leftrightarrow \exists c \in A (b (c) S a (c) \land \forall d \in A (d R c \to b (d) = a (d))))$
65	64	el2v	$⊢ b T a \leftrightarrow \exists c \in A (b (c) S a (c) \land \forall d \in A (d R c \to b (d) = a (d)))$
66	1	wemaplem1	$⊢ (a \in V \land b \in V) \to (a T b \leftrightarrow \exists c \in A (a (c) S b (c) \land \forall d \in A (d R c \to a (d) = b (d))))$
67	66	el2v	$⊢ a T b \leftrightarrow \exists c \in A (a (c) S b (c) \land \forall d \in A (d R c \to a (d) = b (d)))$
68	65 67	orbi12i	$⊢ (b T a \lor a T b) \leftrightarrow (\exists c \in A (b (c) S a (c) \land \forall d \in A (d R c \to b (d) = a (d))) \lor \exists c \in A (a (c) S b (c) \land \forall d \in A (d R c \to a (d) = b (d))))$
69		r19.43	$⊢ \exists c \in A ((b (c) S a (c) \land \forall d \in A (d R c \to b (d) = a (d))) \lor (a (c) S b (c) \land \forall d \in A (d R c \to a (d) = b (d)))) \leftrightarrow (\exists c \in A (b (c) S a (c) \land \forall d \in A (d R c \to b (d) = a (d))) \lor \exists c \in A (a (c) S b (c) \land \forall d \in A (d R c \to a (d) = b (d))))$
70		andir	$⊢ ((b (c) S a (c) \lor a (c) S b (c)) \land \forall d \in A (d R c \to b (d) = a (d))) \leftrightarrow ((b (c) S a (c) \land \forall d \in A (d R c \to b (d) = a (d))) \lor (a (c) S b (c) \land \forall d \in A (d R c \to b (d) = a (d))))$
71		eqcom	$⊢ b (d) = a (d) \leftrightarrow a (d) = b (d)$
72	71	imbi2i	$⊢ (d R c \to b (d) = a (d)) \leftrightarrow (d R c \to a (d) = b (d))$
73	72	ralbii	$⊢ \forall d \in A (d R c \to b (d) = a (d)) \leftrightarrow \forall d \in A (d R c \to a (d) = b (d))$
74	73	anbi2i	$⊢ (a (c) S b (c) \land \forall d \in A (d R c \to b (d) = a (d))) \leftrightarrow (a (c) S b (c) \land \forall d \in A (d R c \to a (d) = b (d)))$
75	74	orbi2i	$⊢ ((b (c) S a (c) \land \forall d \in A (d R c \to b (d) = a (d))) \lor (a (c) S b (c) \land \forall d \in A (d R c \to b (d) = a (d)))) \leftrightarrow ((b (c) S a (c) \land \forall d \in A (d R c \to b (d) = a (d))) \lor (a (c) S b (c) \land \forall d \in A (d R c \to a (d) = b (d))))$
76	70 75	bitr2i	$⊢ ((b (c) S a (c) \land \forall d \in A (d R c \to b (d) = a (d))) \lor (a (c) S b (c) \land \forall d \in A (d R c \to a (d) = b (d)))) \leftrightarrow ((b (c) S a (c) \lor a (c) S b (c)) \land \forall d \in A (d R c \to b (d) = a (d)))$
77	76	rexbii	$⊢ \exists c \in A ((b (c) S a (c) \land \forall d \in A (d R c \to b (d) = a (d))) \lor (a (c) S b (c) \land \forall d \in A (d R c \to a (d) = b (d)))) \leftrightarrow \exists c \in A ((b (c) S a (c) \lor a (c) S b (c)) \land \forall d \in A (d R c \to b (d) = a (d)))$
78	68 69 77	3bitr2i	$⊢ (b T a \lor a T b) \leftrightarrow \exists c \in A ((b (c) S a (c) \lor a (c) S b (c)) \land \forall d \in A (d R c \to b (d) = a (d)))$
79	63 78	sylibr	$⊢ (φ \land ((a \in U \land b \in U) \land a \neq b)) \to (b T a \lor a T b)$
80	79	expr	$⊢ (φ \land (a \in U \land b \in U)) \to (a \neq b \to (b T a \lor a T b))$
81	12 80	biimtrrid	$⊢ (φ \land (a \in U \land b \in U)) \to (\neg a = b \to (b T a \lor a T b))$
82	81	orrd	$⊢ (φ \land (a \in U \land b \in U)) \to (a = b \lor (b T a \lor a T b))$
83		3orrot	$⊢ (a T b \lor a = b \lor b T a) \leftrightarrow (a = b \lor b T a \lor a T b)$
84		3orass	$⊢ (a = b \lor b T a \lor a T b) \leftrightarrow (a = b \lor (b T a \lor a T b))$
85	83 84	bitr2i	$⊢ (a = b \lor (b T a \lor a T b)) \leftrightarrow (a T b \lor a = b \lor b T a)$
86	82 85	sylib	$⊢ (φ \land (a \in U \land b \in U)) \to (a T b \lor a = b \lor b T a)$
87	11 86	issod	$⊢ φ \to T Or U$

Metamath Proof Explorer

Theorem wemapsolem

Proof