Theorem fnwe2lem3 37622

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

Hypotheses

Ref	Expression
fnwe2.su	⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈)
fnwe2.t	⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))}
fnwe2.s	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑈 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑥)})
fnwe2.f	⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶𝐵)
fnwe2.r	⊢ (𝜑 → 𝑅 We 𝐵)
fnwe2lem3.a	⊢ (𝜑 → 𝑎 ∈ 𝐴)
fnwe2lem3.b	⊢ (𝜑 → 𝑏 ∈ 𝐴)

Assertion

Ref	Expression
fnwe2lem3	⊢ (𝜑 → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎))

Distinct variable groups:   𝑦,𝑈,𝑧,𝑎,𝑏   𝑥,𝑆,𝑦,𝑎,𝑏   𝑥,𝑅,𝑦,𝑎,𝑏   𝜑,𝑥,𝑦,𝑧   𝑥,𝐴,𝑦,𝑧,𝑎,𝑏   𝑥,𝐹,𝑦,𝑧,𝑎,𝑏   𝑇,𝑎,𝑏   𝐵,𝑎,𝑏

Allowed substitution hints:   𝜑(𝑎,𝑏)   𝐵(𝑥,𝑦,𝑧)   𝑅(𝑧)   𝑆(𝑧)   𝑇(𝑥,𝑦,𝑧)   𝑈(𝑥)

Proof of Theorem fnwe2lem3

Step	Hyp	Ref	Expression
1		orc 400	. . . . 5 ⊢ ((𝐹‘𝑎)𝑅(𝐹‘𝑏) → ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏)))
2	1	adantl 482	. . . 4 ⊢ ((𝜑 ∧ (𝐹‘𝑎)𝑅(𝐹‘𝑏)) → ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏)))
3		fnwe2.su	. . . . 5 ⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈)
4		fnwe2.t	. . . . 5 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))}
5	3, 4	fnwe2val 37619	. . . 4 ⊢ (𝑎𝑇𝑏 ↔ ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏)))
6	2, 5	sylibr 224	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑎)𝑅(𝐹‘𝑏)) → 𝑎𝑇𝑏)
7	6	3mix1d 1236	. 2 ⊢ ((𝜑 ∧ (𝐹‘𝑎)𝑅(𝐹‘𝑏)) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎))
8		simplr 792	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → (𝐹‘𝑎) = (𝐹‘𝑏))
9		simpr 477	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏)
10	8, 9	jca 554	. . . . . 6 ⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏))
11	10	olcd 408	. . . . 5 ⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏)))
12	11, 5	sylibr 224	. . . 4 ⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → 𝑎𝑇𝑏)
13	12	3mix1d 1236	. . 3 ⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎))
14		3mix2 1231	. . . 4 ⊢ (𝑎 = 𝑏 → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎))
15	14	adantl 482	. . 3 ⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎 = 𝑏) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎))
16		simplr 792	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → (𝐹‘𝑎) = (𝐹‘𝑏))
17	16	eqcomd 2628	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → (𝐹‘𝑏) = (𝐹‘𝑎))
18		csbeq1 3536	. . . . . . . . . 10 ⊢ ((𝐹‘𝑎) = (𝐹‘𝑏) → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 = ⦋(𝐹‘𝑏) / 𝑧⦌𝑆)
19	18	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 = ⦋(𝐹‘𝑏) / 𝑧⦌𝑆)
20	19	breqd 4664	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎 ↔ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎))
21	20	biimpa 501	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎)
22	17, 21	jca 554	. . . . . 6 ⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → ((𝐹‘𝑏) = (𝐹‘𝑎) ∧ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎))
23	22	olcd 408	. . . . 5 ⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → ((𝐹‘𝑏)𝑅(𝐹‘𝑎) ∨ ((𝐹‘𝑏) = (𝐹‘𝑎) ∧ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎)))
24	3, 4	fnwe2val 37619	. . . . 5 ⊢ (𝑏𝑇𝑎 ↔ ((𝐹‘𝑏)𝑅(𝐹‘𝑎) ∨ ((𝐹‘𝑏) = (𝐹‘𝑎) ∧ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎)))
25	23, 24	sylibr 224	. . . 4 ⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → 𝑏𝑇𝑎)
26	25	3mix3d 1238	. . 3 ⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎))
27		fnwe2lem3.a	. . . . . . 7 ⊢ (𝜑 → 𝑎 ∈ 𝐴)
28		fnwe2.s	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑈 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑥)})
29	3, 4, 28	fnwe2lem1 37620	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)})
30	27, 29	mpdan 702	. . . . . 6 ⊢ (𝜑 → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)})
31		weso 5105	. . . . . 6 ⊢ (⦋(𝐹‘𝑎) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)} → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 Or {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)})
32	30, 31	syl 17	. . . . 5 ⊢ (𝜑 → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 Or {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)})
33	32	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 Or {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)})
34	27	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝑎 ∈ 𝐴)
35		eqidd 2623	. . . . 5 ⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘𝑎) = (𝐹‘𝑎))
36		fveq2 6191	. . . . . . 7 ⊢ (𝑦 = 𝑎 → (𝐹‘𝑦) = (𝐹‘𝑎))
37	36	eqeq1d 2624	. . . . . 6 ⊢ (𝑦 = 𝑎 → ((𝐹‘𝑦) = (𝐹‘𝑎) ↔ (𝐹‘𝑎) = (𝐹‘𝑎)))
38	37	elrab 3363	. . . . 5 ⊢ (𝑎 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)} ↔ (𝑎 ∈ 𝐴 ∧ (𝐹‘𝑎) = (𝐹‘𝑎)))
39	34, 35, 38	sylanbrc 698	. . . 4 ⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝑎 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)})
40		fnwe2lem3.b	. . . . . 6 ⊢ (𝜑 → 𝑏 ∈ 𝐴)
41	40	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝑏 ∈ 𝐴)
42		simpr 477	. . . . . 6 ⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘𝑎) = (𝐹‘𝑏))
43	42	eqcomd 2628	. . . . 5 ⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘𝑏) = (𝐹‘𝑎))
44		fveq2 6191	. . . . . . 7 ⊢ (𝑦 = 𝑏 → (𝐹‘𝑦) = (𝐹‘𝑏))
45	44	eqeq1d 2624	. . . . . 6 ⊢ (𝑦 = 𝑏 → ((𝐹‘𝑦) = (𝐹‘𝑎) ↔ (𝐹‘𝑏) = (𝐹‘𝑎)))
46	45	elrab 3363	. . . . 5 ⊢ (𝑏 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)} ↔ (𝑏 ∈ 𝐴 ∧ (𝐹‘𝑏) = (𝐹‘𝑎)))
47	41, 43, 46	sylanbrc 698	. . . 4 ⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝑏 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)})
48		solin 5058	. . . 4 ⊢ ((⦋(𝐹‘𝑎) / 𝑧⦌𝑆 Or {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)} ∧ (𝑎 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)} ∧ 𝑏 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)})) → (𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎))
49	33, 39, 47, 48	syl12anc 1324	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎))
50	13, 15, 26, 49	mpjao3dan 1395	. 2 ⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎))
51		orc 400	. . . . 5 ⊢ ((𝐹‘𝑏)𝑅(𝐹‘𝑎) → ((𝐹‘𝑏)𝑅(𝐹‘𝑎) ∨ ((𝐹‘𝑏) = (𝐹‘𝑎) ∧ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎)))
52	51	adantl 482	. . . 4 ⊢ ((𝜑 ∧ (𝐹‘𝑏)𝑅(𝐹‘𝑎)) → ((𝐹‘𝑏)𝑅(𝐹‘𝑎) ∨ ((𝐹‘𝑏) = (𝐹‘𝑎) ∧ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎)))
53	52, 24	sylibr 224	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑏)𝑅(𝐹‘𝑎)) → 𝑏𝑇𝑎)
54	53	3mix3d 1238	. 2 ⊢ ((𝜑 ∧ (𝐹‘𝑏)𝑅(𝐹‘𝑎)) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎))
55		fnwe2.r	. . . 4 ⊢ (𝜑 → 𝑅 We 𝐵)
56		weso 5105	. . . 4 ⊢ (𝑅 We 𝐵 → 𝑅 Or 𝐵)
57	55, 56	syl 17	. . 3 ⊢ (𝜑 → 𝑅 Or 𝐵)
58		fvres 6207	. . . . 5 ⊢ (𝑎 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑎) = (𝐹‘𝑎))
59	27, 58	syl 17	. . . 4 ⊢ (𝜑 → ((𝐹 ↾ 𝐴)‘𝑎) = (𝐹‘𝑎))
60		fnwe2.f	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶𝐵)
61	60, 27	ffvelrnd 6360	. . . 4 ⊢ (𝜑 → ((𝐹 ↾ 𝐴)‘𝑎) ∈ 𝐵)
62	59, 61	eqeltrrd 2702	. . 3 ⊢ (𝜑 → (𝐹‘𝑎) ∈ 𝐵)
63		fvres 6207	. . . . 5 ⊢ (𝑏 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑏) = (𝐹‘𝑏))
64	40, 63	syl 17	. . . 4 ⊢ (𝜑 → ((𝐹 ↾ 𝐴)‘𝑏) = (𝐹‘𝑏))
65	60, 40	ffvelrnd 6360	. . . 4 ⊢ (𝜑 → ((𝐹 ↾ 𝐴)‘𝑏) ∈ 𝐵)
66	64, 65	eqeltrrd 2702	. . 3 ⊢ (𝜑 → (𝐹‘𝑏) ∈ 𝐵)
67		solin 5058	. . 3 ⊢ ((𝑅 Or 𝐵 ∧ ((𝐹‘𝑎) ∈ 𝐵 ∧ (𝐹‘𝑏) ∈ 𝐵)) → ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑎) = (𝐹‘𝑏) ∨ (𝐹‘𝑏)𝑅(𝐹‘𝑎)))
68	57, 62, 66, 67	syl12anc 1324	. 2 ⊢ (𝜑 → ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑎) = (𝐹‘𝑏) ∨ (𝐹‘𝑏)𝑅(𝐹‘𝑎)))
69	7, 50, 54, 68	mpjao3dan 1395	1 ⊢ (𝜑 → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎))

Syntax hints:   → wi 4   ∨ wo 383   ∧ wa 384   ∨ w3o 1036   = wceq 1483   ∈ wcel 1990  {crab 2916  ⦋csb 3533   class class class wbr 4653  {copab 4712   Or wor 5034   We wwe 5072   ↾ cres 5116  ⟶wf 5884  ‘cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896

This theorem is referenced by:  fnwe2  37623