fnwe2lem3

Description: Lemma for fnwe2 . Trichotomy. (Contributed by Stefan O'Rear, 19-Jan-2015)

	Ref	Expression
Hypotheses	fnwe2.su	$⊢ z = F (x) \to S = U$
	fnwe2.t	$⊢ T = \{⟨x, y⟩ \| (F (x) R F (y) \lor (F (x) = F (y) \land x U y))\}$
	fnwe2.s	$⊢ (φ \land x \in A) \to U We \{y \in A \| F (y) = F (x)\}$
	fnwe2.f	$⊢ φ \to ({F ↾}_{A}) : A ⟶ B$
	fnwe2.r	$⊢ φ \to R We B$
	fnwe2lem3.a	$⊢ φ \to a \in A$
	fnwe2lem3.b	$⊢ φ \to b \in A$
Assertion	fnwe2lem3	$⊢ φ \to (a T b \lor a = b \lor b T a)$

Proof

Step	Hyp	Ref	Expression
1		fnwe2.su	$⊢ z = F (x) \to S = U$
2		fnwe2.t	$⊢ T = \{⟨x, y⟩ \| (F (x) R F (y) \lor (F (x) = F (y) \land x U y))\}$
3		fnwe2.s	$⊢ (φ \land x \in A) \to U We \{y \in A \| F (y) = F (x)\}$
4		fnwe2.f	$⊢ φ \to ({F ↾}_{A}) : A ⟶ B$
5		fnwe2.r	$⊢ φ \to R We B$
6		fnwe2lem3.a	$⊢ φ \to a \in A$
7		fnwe2lem3.b	$⊢ φ \to b \in A$
8		animorrl	$⊢ (φ \land F (a) R F (b)) \to (F (a) R F (b) \lor (F (a) = F (b) \land a ⦋ F (a) / z ⦌ S b))$
9	1 2	fnwe2val	$⊢ a T b \leftrightarrow (F (a) R F (b) \lor (F (a) = F (b) \land a ⦋ F (a) / z ⦌ S b))$
10	8 9	sylibr	$⊢ (φ \land F (a) R F (b)) \to a T b$
11	10	3mix1d	$⊢ (φ \land F (a) R F (b)) \to (a T b \lor a = b \lor b T a)$
12		simplr	$⊢ ((φ \land F (a) = F (b)) \land a ⦋ F (a) / z ⦌ S b) \to F (a) = F (b)$
13		simpr	$⊢ ((φ \land F (a) = F (b)) \land a ⦋ F (a) / z ⦌ S b) \to a ⦋ F (a) / z ⦌ S b$
14	12 13	jca	$⊢ ((φ \land F (a) = F (b)) \land a ⦋ F (a) / z ⦌ S b) \to (F (a) = F (b) \land a ⦋ F (a) / z ⦌ S b)$
15	14	olcd	$⊢ ((φ \land F (a) = F (b)) \land a ⦋ F (a) / z ⦌ S b) \to (F (a) R F (b) \lor (F (a) = F (b) \land a ⦋ F (a) / z ⦌ S b))$
16	15 9	sylibr	$⊢ ((φ \land F (a) = F (b)) \land a ⦋ F (a) / z ⦌ S b) \to a T b$
17	16	3mix1d	$⊢ ((φ \land F (a) = F (b)) \land a ⦋ F (a) / z ⦌ S b) \to (a T b \lor a = b \lor b T a)$
18		3mix2	$⊢ a = b \to (a T b \lor a = b \lor b T a)$
19	18	adantl	$⊢ ((φ \land F (a) = F (b)) \land a = b) \to (a T b \lor a = b \lor b T a)$
20		simplr	$⊢ ((φ \land F (a) = F (b)) \land b ⦋ F (a) / z ⦌ S a) \to F (a) = F (b)$
21	20	eqcomd	$⊢ ((φ \land F (a) = F (b)) \land b ⦋ F (a) / z ⦌ S a) \to F (b) = F (a)$
22		csbeq1	$⊢ F (a) = F (b) \to ⦋ F (a) / z ⦌ S = ⦋ F (b) / z ⦌ S$
23	22	adantl	$⊢ (φ \land F (a) = F (b)) \to ⦋ F (a) / z ⦌ S = ⦋ F (b) / z ⦌ S$
24	23	breqd	$⊢ (φ \land F (a) = F (b)) \to (b ⦋ F (a) / z ⦌ S a \leftrightarrow b ⦋ F (b) / z ⦌ S a)$
25	24	biimpa	$⊢ ((φ \land F (a) = F (b)) \land b ⦋ F (a) / z ⦌ S a) \to b ⦋ F (b) / z ⦌ S a$
26	21 25	jca	$⊢ ((φ \land F (a) = F (b)) \land b ⦋ F (a) / z ⦌ S a) \to (F (b) = F (a) \land b ⦋ F (b) / z ⦌ S a)$
27	26	olcd	$⊢ ((φ \land F (a) = F (b)) \land b ⦋ F (a) / z ⦌ S a) \to (F (b) R F (a) \lor (F (b) = F (a) \land b ⦋ F (b) / z ⦌ S a))$
28	1 2	fnwe2val	$⊢ b T a \leftrightarrow (F (b) R F (a) \lor (F (b) = F (a) \land b ⦋ F (b) / z ⦌ S a))$
29	27 28	sylibr	$⊢ ((φ \land F (a) = F (b)) \land b ⦋ F (a) / z ⦌ S a) \to b T a$
30	29	3mix3d	$⊢ ((φ \land F (a) = F (b)) \land b ⦋ F (a) / z ⦌ S a) \to (a T b \lor a = b \lor b T a)$
31	1 2 3	fnwe2lem1	$⊢ (φ \land a \in A) \to ⦋ F (a) / z ⦌ S We \{y \in A \| F (y) = F (a)\}$
32	6 31	mpdan	$⊢ φ \to ⦋ F (a) / z ⦌ S We \{y \in A \| F (y) = F (a)\}$
33		weso	$⊢ ⦋ F (a) / z ⦌ S We \{y \in A \| F (y) = F (a)\} \to ⦋ F (a) / z ⦌ S Or \{y \in A \| F (y) = F (a)\}$
34	32 33	syl	$⊢ φ \to ⦋ F (a) / z ⦌ S Or \{y \in A \| F (y) = F (a)\}$
35	34	adantr	$⊢ (φ \land F (a) = F (b)) \to ⦋ F (a) / z ⦌ S Or \{y \in A \| F (y) = F (a)\}$
36		fveqeq2	$⊢ y = a \to (F (y) = F (a) \leftrightarrow F (a) = F (a))$
37	6	adantr	$⊢ (φ \land F (a) = F (b)) \to a \in A$
38		eqidd	$⊢ (φ \land F (a) = F (b)) \to F (a) = F (a)$
39	36 37 38	elrabd	$⊢ (φ \land F (a) = F (b)) \to a \in \{y \in A \| F (y) = F (a)\}$
40		fveqeq2	$⊢ y = b \to (F (y) = F (a) \leftrightarrow F (b) = F (a))$
41	7	adantr	$⊢ (φ \land F (a) = F (b)) \to b \in A$
42		simpr	$⊢ (φ \land F (a) = F (b)) \to F (a) = F (b)$
43	42	eqcomd	$⊢ (φ \land F (a) = F (b)) \to F (b) = F (a)$
44	40 41 43	elrabd	$⊢ (φ \land F (a) = F (b)) \to b \in \{y \in A \| F (y) = F (a)\}$
45		solin	$⊢ (⦋ F (a) / z ⦌ S Or \{y \in A \| F (y) = F (a)\} \land (a \in \{y \in A \| F (y) = F (a)\} \land b \in \{y \in A \| F (y) = F (a)\})) \to (a ⦋ F (a) / z ⦌ S b \lor a = b \lor b ⦋ F (a) / z ⦌ S a)$
46	35 39 44 45	syl12anc	$⊢ (φ \land F (a) = F (b)) \to (a ⦋ F (a) / z ⦌ S b \lor a = b \lor b ⦋ F (a) / z ⦌ S a)$
47	17 19 30 46	mpjao3dan	$⊢ (φ \land F (a) = F (b)) \to (a T b \lor a = b \lor b T a)$
48		animorrl	$⊢ (φ \land F (b) R F (a)) \to (F (b) R F (a) \lor (F (b) = F (a) \land b ⦋ F (b) / z ⦌ S a))$
49	48 28	sylibr	$⊢ (φ \land F (b) R F (a)) \to b T a$
50	49	3mix3d	$⊢ (φ \land F (b) R F (a)) \to (a T b \lor a = b \lor b T a)$
51		weso	$⊢ R We B \to R Or B$
52	5 51	syl	$⊢ φ \to R Or B$
53	6	fvresd	$⊢ φ \to ({F ↾}_{A}) (a) = F (a)$
54	4 6	ffvelrnd	$⊢ φ \to ({F ↾}_{A}) (a) \in B$
55	53 54	eqeltrrd	$⊢ φ \to F (a) \in B$
56	7	fvresd	$⊢ φ \to ({F ↾}_{A}) (b) = F (b)$
57	4 7	ffvelrnd	$⊢ φ \to ({F ↾}_{A}) (b) \in B$
58	56 57	eqeltrrd	$⊢ φ \to F (b) \in B$
59		solin	$⊢ (R Or B \land (F (a) \in B \land F (b) \in B)) \to (F (a) R F (b) \lor F (a) = F (b) \lor F (b) R F (a))$
60	52 55 58 59	syl12anc	$⊢ φ \to (F (a) R F (b) \lor F (a) = F (b) \lor F (b) R F (a))$
61	11 47 50 60	mpjao3dan	$⊢ φ \to (a T b \lor a = b \lor b T a)$

Metamath Proof Explorer

Theorem fnwe2lem3

Proof