Theorem fnwe2lem2 43811

Description: Lemma for fnwe2 43813. An element which is in a minimal fiber and minimal within its fiber is minimal globally; thus 𝑇 is well-founded. (Contributed by Stefan O'Rear, 19-Jan-2015.)

Hypotheses

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

Assertion

Ref	Expression
fnwe2lem2	⊢ (𝜑 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)

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

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

Proof of Theorem fnwe2lem2

Dummy variables 𝑑 𝑒 𝑓 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fnwe2.f	. . . 4 ⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶𝐵)
2		ffun 6712	. . . 4 ⊢ ((𝐹 ↾ 𝐴):𝐴⟶𝐵 → Fun (𝐹 ↾ 𝐴))
3		vex 3461	. . . . 5 ⊢ 𝑎 ∈ V
4	3	funimaex 6627	. . . 4 ⊢ (Fun (𝐹 ↾ 𝐴) → ((𝐹 ↾ 𝐴) “ 𝑎) ∈ V)
5	1, 2, 4	3syl 19	. . 3 ⊢ (𝜑 → ((𝐹 ↾ 𝐴) “ 𝑎) ∈ V)
6		fnwe2.r	. . . 4 ⊢ (𝜑 → 𝑅 We 𝐵)
7		wefr 5653	. . . 4 ⊢ (𝑅 We 𝐵 → 𝑅 Fr 𝐵)
8	6, 7	syl 18	. . 3 ⊢ (𝜑 → 𝑅 Fr 𝐵)
9		imassrn 6075	. . . 4 ⊢ ((𝐹 ↾ 𝐴) “ 𝑎) ⊆ ran (𝐹 ↾ 𝐴)
10	1	frnd 6718	. . . 4 ⊢ (𝜑 → ran (𝐹 ↾ 𝐴) ⊆ 𝐵)
11	9, 10	sstrid 3949	. . 3 ⊢ (𝜑 → ((𝐹 ↾ 𝐴) “ 𝑎) ⊆ 𝐵)
12		incom 4162	. . . . . 6 ⊢ (dom (𝐹 ↾ 𝐴) ∩ 𝑎) = (𝑎 ∩ dom (𝐹 ↾ 𝐴))
13		fnwe2lem2.a	. . . . . . . 8 ⊢ (𝜑 → 𝑎 ⊆ 𝐴)
14	1	fdmd 6720	. . . . . . . 8 ⊢ (𝜑 → dom (𝐹 ↾ 𝐴) = 𝐴)
15	13, 14	sseqtrrd 3975	. . . . . . 7 ⊢ (𝜑 → 𝑎 ⊆ dom (𝐹 ↾ 𝐴))
16		dfss2 3924	. . . . . . 7 ⊢ (𝑎 ⊆ dom (𝐹 ↾ 𝐴) ↔ (𝑎 ∩ dom (𝐹 ↾ 𝐴)) = 𝑎)
17	15, 16	sylib 221	. . . . . 6 ⊢ (𝜑 → (𝑎 ∩ dom (𝐹 ↾ 𝐴)) = 𝑎)
18	12, 17	eqtrid 2812	. . . . 5 ⊢ (𝜑 → (dom (𝐹 ↾ 𝐴) ∩ 𝑎) = 𝑎)
19		fnwe2lem2.n0	. . . . 5 ⊢ (𝜑 → 𝑎 ≠ ∅)
20	18, 19	eqnetrd 3027	. . . 4 ⊢ (𝜑 → (dom (𝐹 ↾ 𝐴) ∩ 𝑎) ≠ ∅)
21		imadisj 6084	. . . . 5 ⊢ (((𝐹 ↾ 𝐴) “ 𝑎) = ∅ ↔ (dom (𝐹 ↾ 𝐴) ∩ 𝑎) = ∅)
22	21	necon3bii 3012	. . . 4 ⊢ (((𝐹 ↾ 𝐴) “ 𝑎) ≠ ∅ ↔ (dom (𝐹 ↾ 𝐴) ∩ 𝑎) ≠ ∅)
23	20, 22	sylibr 237	. . 3 ⊢ (𝜑 → ((𝐹 ↾ 𝐴) “ 𝑎) ≠ ∅)
24		fri 5621	. . 3 ⊢ (((((𝐹 ↾ 𝐴) “ 𝑎) ∈ V ∧ 𝑅 Fr 𝐵) ∧ (((𝐹 ↾ 𝐴) “ 𝑎) ⊆ 𝐵 ∧ ((𝐹 ↾ 𝐴) “ 𝑎) ≠ ∅)) → ∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
25	5, 8, 11, 23, 24	syl22anc 852	. 2 ⊢ (𝜑 → ∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
26		df-ima 5676	. . . . . 6 ⊢ ((𝐹 ↾ 𝐴) “ 𝑎) = ran ((𝐹 ↾ 𝐴) ↾ 𝑎)
27	26	rexeqi 3324	. . . . 5 ⊢ (∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑑 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
28	1	ffnd 6710	. . . . . . 7 ⊢ (𝜑 → (𝐹 ↾ 𝐴) Fn 𝐴)
29		fnssres 6662	. . . . . . 7 ⊢ (((𝐹 ↾ 𝐴) Fn 𝐴 ∧ 𝑎 ⊆ 𝐴) → ((𝐹 ↾ 𝐴) ↾ 𝑎) Fn 𝑎)
30	28, 13, 29	syl2anc 596	. . . . . 6 ⊢ (𝜑 → ((𝐹 ↾ 𝐴) ↾ 𝑎) Fn 𝑎)
31		breq2 5115	. . . . . . . . 9 ⊢ (𝑑 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) → (𝑒𝑅𝑑 ↔ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
32	31	notbid 321	. . . . . . . 8 ⊢ (𝑑 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) → (¬ 𝑒𝑅𝑑 ↔ ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
33	32	ralbidv 3190	. . . . . . 7 ⊢ (𝑑 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) → (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
34	33	rexrn 7086	. . . . . 6 ⊢ (((𝐹 ↾ 𝐴) ↾ 𝑎) Fn 𝑎 → (∃𝑑 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓 ∈ 𝑎 ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
35	30, 34	syl 18	. . . . 5 ⊢ (𝜑 → (∃𝑑 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓 ∈ 𝑎 ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
36	27, 35	bitrid 286	. . . 4 ⊢ (𝜑 → (∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓 ∈ 𝑎 ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
37	26	raleqi 3323	. . . . . . . 8 ⊢ (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑒 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓))
38		breq1 5114	. . . . . . . . . . 11 ⊢ (𝑒 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑) → (𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
39	38	notbid 321	. . . . . . . . . 10 ⊢ (𝑒 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑) → (¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
40	39	ralrn 7087	. . . . . . . . 9 ⊢ (((𝐹 ↾ 𝐴) ↾ 𝑎) Fn 𝑎 → (∀𝑒 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
41	30, 40	syl 18	. . . . . . . 8 ⊢ (𝜑 → (∀𝑒 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
42	37, 41	bitrid 286	. . . . . . 7 ⊢ (𝜑 → (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
43	42	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
44	13	resabs1d 6009	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐹 ↾ 𝐴) ↾ 𝑎) = (𝐹 ↾ 𝑎))
45	44	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → ((𝐹 ↾ 𝐴) ↾ 𝑎) = (𝐹 ↾ 𝑎))
46	45	fveq1d 6887	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑) = ((𝐹 ↾ 𝑎)‘𝑑))
47		fvres 6904	. . . . . . . . . . 11 ⊢ (𝑑 ∈ 𝑎 → ((𝐹 ↾ 𝑎)‘𝑑) = (𝐹‘𝑑))
48	47	adantl 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → ((𝐹 ↾ 𝑎)‘𝑑) = (𝐹‘𝑑))
49	46, 48	eqtrd 2800	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑) = (𝐹‘𝑑))
50	45	fveq1d 6887	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) = ((𝐹 ↾ 𝑎)‘𝑓))
51		fvres 6904	. . . . . . . . . . 11 ⊢ (𝑓 ∈ 𝑎 → ((𝐹 ↾ 𝑎)‘𝑓) = (𝐹‘𝑓))
52	51	ad2antlr 740	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → ((𝐹 ↾ 𝑎)‘𝑓) = (𝐹‘𝑓))
53	50, 52	eqtrd 2800	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) = (𝐹‘𝑓))
54	49, 53	breq12d 5124	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → ((((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
55	54	notbid 321	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
56	55	ralbidva 3188	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → (∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
57	43, 56	bitrd 282	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
58	57	rexbidva 3189	. . . 4 ⊢ (𝜑 → (∃𝑓 ∈ 𝑎 ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∃𝑓 ∈ 𝑎 ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
59	36, 58	bitrd 282	. . 3 ⊢ (𝜑 → (∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓 ∈ 𝑎 ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
60	3	inex1 5288	. . . . . . 7 ⊢ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ∈ V
61	60	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ∈ V)
62	13	sselda 3938	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → 𝑓 ∈ 𝐴)
63		fnwe2.su	. . . . . . . . . 10 ⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈)
64		fnwe2.t	. . . . . . . . . 10 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))}
65		fnwe2.s	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑈 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑥)})
66	63, 64, 65	fnwe2lem1 43810	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
67		wefr 5653	. . . . . . . . 9 ⊢ (⦋(𝐹‘𝑓) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)} → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 Fr {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
68	66, 67	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 Fr {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
69	62, 68	syldan 603	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 Fr {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
70	69	adantrr 730	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 Fr {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
71		inss2 4190	. . . . . . 7 ⊢ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ⊆ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}
72	71	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ⊆ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
73		simprl 783	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → 𝑓 ∈ 𝑎)
74		fveqeq2 6894	. . . . . . . . 9 ⊢ (𝑦 = 𝑓 → ((𝐹‘𝑦) = (𝐹‘𝑓) ↔ (𝐹‘𝑓) = (𝐹‘𝑓)))
75	62	adantrr 730	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → 𝑓 ∈ 𝐴)
76		eqidd 2766	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝐹‘𝑓) = (𝐹‘𝑓))
77	74, 75, 76	elrabd 3654	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → 𝑓 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
78	73, 77	elind 4153	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → 𝑓 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}))
79	78	ne0d 4295	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ≠ ∅)
80		fri 5621	. . . . . 6 ⊢ ((((𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ∈ V ∧ ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 Fr {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ∧ ((𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ⊆ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)} ∧ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ≠ ∅)) → ∃𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)
81	61, 70, 72, 79, 80	syl22anc 852	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → ∃𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)
82		elin 3922	. . . . . . . 8 ⊢ (𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑒 ∈ 𝑎 ∧ 𝑒 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}))
83		fveqeq2 6894	. . . . . . . . . 10 ⊢ (𝑦 = 𝑒 → ((𝐹‘𝑦) = (𝐹‘𝑓) ↔ (𝐹‘𝑒) = (𝐹‘𝑓)))
84	83	elrab 3652	. . . . . . . . 9 ⊢ (𝑒 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)} ↔ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))
85	84	anbi2i 635	. . . . . . . 8 ⊢ ((𝑒 ∈ 𝑎 ∧ 𝑒 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓))))
86	82, 85	bitri 278	. . . . . . 7 ⊢ (𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓))))
87		elin 3922	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑔 ∈ 𝑎 ∧ 𝑔 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}))
88		fveqeq2 6894	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑔 → ((𝐹‘𝑦) = (𝐹‘𝑓) ↔ (𝐹‘𝑔) = (𝐹‘𝑓)))
89	88	elrab 3652	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)} ↔ (𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)))
90	89	anbi2i 635	. . . . . . . . . . . . 13 ⊢ ((𝑔 ∈ 𝑎 ∧ 𝑔 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑔 ∈ 𝑎 ∧ (𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓))))
91	87, 90	bitri 278	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑔 ∈ 𝑎 ∧ (𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓))))
92	91	imbi1i 352	. . . . . . . . . . 11 ⊢ ((𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) ↔ ((𝑔 ∈ 𝑎 ∧ (𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓))) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))
93		impexp 456	. . . . . . . . . . 11 ⊢ (((𝑔 ∈ 𝑎 ∧ (𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓))) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) ↔ (𝑔 ∈ 𝑎 → ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)))
94	92, 93	bitri 278	. . . . . . . . . 10 ⊢ ((𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) ↔ (𝑔 ∈ 𝑎 → ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)))
95	94	ralbii2 3109	. . . . . . . . 9 ⊢ (∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 ↔ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))
96		simplrl 789	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) → 𝑒 ∈ 𝑎)
97		fveq2 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑐 → (𝐹‘𝑑) = (𝐹‘𝑐))
98	97	breq1d 5121	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑐 → ((𝐹‘𝑑)𝑅(𝐹‘𝑓) ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑓)))
99	98	notbid 321	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑐 → (¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓) ↔ ¬ (𝐹‘𝑐)𝑅(𝐹‘𝑓)))
100		simplrr 790	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) → ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))
101	100	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))
102		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → 𝑐 ∈ 𝑎)
103	99, 101, 102	rspcdva 3584	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ (𝐹‘𝑐)𝑅(𝐹‘𝑓))
104		simprrr 794	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) → (𝐹‘𝑒) = (𝐹‘𝑓))
105	104	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → (𝐹‘𝑒) = (𝐹‘𝑓))
106	105	breq2d 5123	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ((𝐹‘𝑐)𝑅(𝐹‘𝑒) ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑓)))
107	103, 106	mtbird 328	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ (𝐹‘𝑐)𝑅(𝐹‘𝑒))
108	13	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) → 𝑎 ⊆ 𝐴)
109	108	sselda 3938	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → 𝑐 ∈ 𝐴)
110	109	adantrr 730	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → 𝑐 ∈ 𝐴)
111		simprr 785	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝐹‘𝑐) = (𝐹‘𝑒))
112	104	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝐹‘𝑒) = (𝐹‘𝑓))
113	111, 112	eqtrd 2800	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝐹‘𝑐) = (𝐹‘𝑓))
114		eleq1w 2848	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑐 → (𝑔 ∈ 𝐴 ↔ 𝑐 ∈ 𝐴))
115		fveqeq2 6894	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑐 → ((𝐹‘𝑔) = (𝐹‘𝑓) ↔ (𝐹‘𝑐) = (𝐹‘𝑓)))
116	114, 115	anbi12d 644	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑐 → ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) ↔ (𝑐 ∈ 𝐴 ∧ (𝐹‘𝑐) = (𝐹‘𝑓))))
117		breq1 5114	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑐 → (𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 ↔ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))
118	117	notbid 321	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑐 → (¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 ↔ ¬ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))
119	116, 118	imbi12d 347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑐 → (((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) ↔ ((𝑐 ∈ 𝐴 ∧ (𝐹‘𝑐) = (𝐹‘𝑓)) → ¬ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)))
120		simplr 781	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))
121		simprl 783	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → 𝑐 ∈ 𝑎)
122	119, 120, 121	rspcdva 3584	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ((𝑐 ∈ 𝐴 ∧ (𝐹‘𝑐) = (𝐹‘𝑓)) → ¬ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))
123	110, 113, 122	mp2and 712	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ¬ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)
124	111, 112	eqtr2d 2801	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝐹‘𝑓) = (𝐹‘𝑐))
125	124	csbeq1d 3858	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 = ⦋(𝐹‘𝑐) / 𝑧⦌𝑆)
126	125	breqd 5122	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 ↔ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒))
127	123, 126	mtbid 327	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ¬ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒)
128	127	expr 462	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ((𝐹‘𝑐) = (𝐹‘𝑒) → ¬ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒))
129		imnan 405	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑐) = (𝐹‘𝑒) → ¬ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒) ↔ ¬ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒))
130	128, 129	sylib 221	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒))
131		ioran 999	. . . . . . . . . . . . . 14 ⊢ (¬ ((𝐹‘𝑐)𝑅(𝐹‘𝑒) ∨ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒)) ↔ (¬ (𝐹‘𝑐)𝑅(𝐹‘𝑒) ∧ ¬ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒)))
132	107, 130, 131	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ ((𝐹‘𝑐)𝑅(𝐹‘𝑒) ∨ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒)))
133	63, 64	fnwe2val 43809	. . . . . . . . . . . . 13 ⊢ (𝑐𝑇𝑒 ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑒) ∨ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒)))
134	132, 133	sylnibr 332	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ 𝑐𝑇𝑒)
135	134	ralrimiva 3159	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) → ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑒)
136		breq2 5115	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑒 → (𝑐𝑇𝑏 ↔ 𝑐𝑇𝑒))
137	136	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑒 → (¬ 𝑐𝑇𝑏 ↔ ¬ 𝑐𝑇𝑒))
138	137	ralbidv 3190	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑒 → (∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏 ↔ ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑒))
139	138	rspcev 3583	. . . . . . . . . . 11 ⊢ ((𝑒 ∈ 𝑎 ∧ ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑒) → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)
140	96, 135, 139	syl2anc 596	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)
141	140	ex 418	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) → (∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏))
142	95, 141	biimtrid 245	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) → (∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏))
143	142	ex 418	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → ((𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓))) → (∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)))
144	86, 143	biimtrid 245	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) → (∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)))
145	144	rexlimdv 3166	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (∃𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏))
146	81, 145	mpd 16	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)
147	146	rexlimdvaa 3169	. . 3 ⊢ (𝜑 → (∃𝑓 ∈ 𝑎 ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓) → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏))
148	59, 147	sylbid 243	. 2 ⊢ (𝜑 → (∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏))
149	25, 148	mpd 16	1 ⊢ (𝜑 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2146   ≠ wne 2960  ∀wral 3081  ∃wrex 3091  {crab 3418  Vcvv 3457  ⦋csb 3854   ∩ cin 3905   ⊆ wss 3906  ∅c0 4286   class class class wbr 5111  {copab 5175   Fr wfr 5613   We wwe 5615  dom cdm 5663  ran crn 5664   ↾ cres 5665   “ cima 5666  Fun wfun 6534   Fn wfn 6535  ⟶wf 6536  ‘cfv 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548

This theorem is used by:  fnwe2  43813