Theorem fnwe2lem2 44037

Description: Lemma for fnwe2 44039. 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 6710	. . . 4 ⊢ ((𝐹 ↾ 𝐴):𝐴⟶𝐵 → Fun (𝐹 ↾ 𝐴))
3		vex 3455	. . . . 5 ⊢ 𝑎 ∈ V
4	3	funimaex 6625	. . . 4 ⊢ (Fun (𝐹 ↾ 𝐴) → ((𝐹 ↾ 𝐴) “ 𝑎) ∈ V)
5	1, 2, 4	3syl 19	. . 3 ⊢ (𝜑 → ((𝐹 ↾ 𝐴) “ 𝑎) ∈ V)
6		fnwe2.r	. . . 4 ⊢ (𝜑 → 𝑅 We 𝐵)
7		wefr 5641	. . . 4 ⊢ (𝑅 We 𝐵 → 𝑅 Fr 𝐵)
8	6, 7	syl 18	. . 3 ⊢ (𝜑 → 𝑅 Fr 𝐵)
9		imassrn 6196	. . . 4 ⊢ ((𝐹 ↾ 𝐴) “ 𝑎) ⊆ ran (𝐹 ↾ 𝐴)
10	1	frnd 6716	. . . 4 ⊢ (𝜑 → ran (𝐹 ↾ 𝐴) ⊆ 𝐵)
11	9, 10	sstrid 3942	. . 3 ⊢ (𝜑 → ((𝐹 ↾ 𝐴) “ 𝑎) ⊆ 𝐵)
12		incom 4155	. . . . . 6 ⊢ (dom (𝐹 ↾ 𝐴) ∩ 𝑎) = (𝑎 ∩ dom (𝐹 ↾ 𝐴))
13		fnwe2lem2.a	. . . . . . . 8 ⊢ (𝜑 → 𝑎 ⊆ 𝐴)
14	1	fdmd 6718	. . . . . . . 8 ⊢ (𝜑 → dom (𝐹 ↾ 𝐴) = 𝐴)
15	13, 14	sseqtrrd 3968	. . . . . . 7 ⊢ (𝜑 → 𝑎 ⊆ dom (𝐹 ↾ 𝐴))
16		dfss2 3917	. . . . . . 7 ⊢ (𝑎 ⊆ dom (𝐹 ↾ 𝐴) ↔ (𝑎 ∩ dom (𝐹 ↾ 𝐴)) = 𝑎)
17	15, 16	sylib 221	. . . . . 6 ⊢ (𝜑 → (𝑎 ∩ dom (𝐹 ↾ 𝐴)) = 𝑎)
18	12, 17	eqtrid 2808	. . . . 5 ⊢ (𝜑 → (dom (𝐹 ↾ 𝐴) ∩ 𝑎) = 𝑎)
19		fnwe2lem2.n0	. . . . 5 ⊢ (𝜑 → 𝑎 ≠ ∅)
20	18, 19	eqnetrd 3023	. . . 4 ⊢ (𝜑 → (dom (𝐹 ↾ 𝐴) ∩ 𝑎) ≠ ∅)
21		imadisj 6077	. . . . 5 ⊢ (((𝐹 ↾ 𝐴) “ 𝑎) = ∅ ↔ (dom (𝐹 ↾ 𝐴) ∩ 𝑎) = ∅)
22	21	necon3bii 3008	. . . 4 ⊢ (((𝐹 ↾ 𝐴) “ 𝑎) ≠ ∅ ↔ (dom (𝐹 ↾ 𝐴) ∩ 𝑎) ≠ ∅)
23	20, 22	sylibr 237	. . 3 ⊢ (𝜑 → ((𝐹 ↾ 𝐴) “ 𝑎) ≠ ∅)
24		fri 5609	. . 3 ⊢ (((((𝐹 ↾ 𝐴) “ 𝑎) ∈ V ∧ 𝑅 Fr 𝐵) ∧ (((𝐹 ↾ 𝐴) “ 𝑎) ⊆ 𝐵 ∧ ((𝐹 ↾ 𝐴) “ 𝑎) ≠ ∅)) → ∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
25	5, 8, 11, 23, 24	syl22anc 852	. 2 ⊢ (𝜑 → ∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
26		df-ima 5664	. . . . . 6 ⊢ ((𝐹 ↾ 𝐴) “ 𝑎) = ran ((𝐹 ↾ 𝐴) ↾ 𝑎)
27	26	rexeqi 3319	. . . . 5 ⊢ (∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑑 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
28	1	ffnd 6708	. . . . . . 7 ⊢ (𝜑 → (𝐹 ↾ 𝐴) Fn 𝐴)
29		fnssres 6660	. . . . . . 7 ⊢ (((𝐹 ↾ 𝐴) Fn 𝐴 ∧ 𝑎 ⊆ 𝐴) → ((𝐹 ↾ 𝐴) ↾ 𝑎) Fn 𝑎)
30	28, 13, 29	syl2anc 596	. . . . . 6 ⊢ (𝜑 → ((𝐹 ↾ 𝐴) ↾ 𝑎) Fn 𝑎)
31		breq2 5107	. . . . . . . . 9 ⊢ (𝑑 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) → (𝑒𝑅𝑑 ↔ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
32	31	notbid 321	. . . . . . . 8 ⊢ (𝑑 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) → (¬ 𝑒𝑅𝑑 ↔ ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
33	32	ralbidv 3186	. . . . . . 7 ⊢ (𝑑 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) → (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
34	33	rexrn 7085	. . . . . 6 ⊢ (((𝐹 ↾ 𝐴) ↾ 𝑎) Fn 𝑎 → (∃𝑑 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓 ∈ 𝑎 ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
35	30, 34	syl 18	. . . . 5 ⊢ (𝜑 → (∃𝑑 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓 ∈ 𝑎 ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
36	27, 35	bitrid 286	. . . 4 ⊢ (𝜑 → (∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓 ∈ 𝑎 ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
37	26	raleqi 3318	. . . . . . . 8 ⊢ (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑒 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓))
38		breq1 5106	. . . . . . . . . . 11 ⊢ (𝑒 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑) → (𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
39	38	notbid 321	. . . . . . . . . 10 ⊢ (𝑒 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑) → (¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
40	39	ralrn 7086	. . . . . . . . 9 ⊢ (((𝐹 ↾ 𝐴) ↾ 𝑎) Fn 𝑎 → (∀𝑒 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
41	30, 40	syl 18	. . . . . . . 8 ⊢ (𝜑 → (∀𝑒 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
42	37, 41	bitrid 286	. . . . . . 7 ⊢ (𝜑 → (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
43	42	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
44	13	resabs1d 5999	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐹 ↾ 𝐴) ↾ 𝑎) = (𝐹 ↾ 𝑎))
45	44	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → ((𝐹 ↾ 𝐴) ↾ 𝑎) = (𝐹 ↾ 𝑎))
46	45	fveq1d 6885	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑) = ((𝐹 ↾ 𝑎)‘𝑑))
47		fvres 6902	. . . . . . . . . . 11 ⊢ (𝑑 ∈ 𝑎 → ((𝐹 ↾ 𝑎)‘𝑑) = (𝐹‘𝑑))
48	47	adantl 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → ((𝐹 ↾ 𝑎)‘𝑑) = (𝐹‘𝑑))
49	46, 48	eqtrd 2796	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑) = (𝐹‘𝑑))
50	45	fveq1d 6885	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) = ((𝐹 ↾ 𝑎)‘𝑓))
51		fvres 6902	. . . . . . . . . . 11 ⊢ (𝑓 ∈ 𝑎 → ((𝐹 ↾ 𝑎)‘𝑓) = (𝐹‘𝑓))
52	51	ad2antlr 740	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → ((𝐹 ↾ 𝑎)‘𝑓) = (𝐹‘𝑓))
53	50, 52	eqtrd 2796	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) = (𝐹‘𝑓))
54	49, 53	breq12d 5116	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → ((((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
55	54	notbid 321	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
56	55	ralbidva 3184	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → (∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
57	43, 56	bitrd 282	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
58	57	rexbidva 3185	. . . 4 ⊢ (𝜑 → (∃𝑓 ∈ 𝑎 ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∃𝑓 ∈ 𝑎 ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
59	36, 58	bitrd 282	. . 3 ⊢ (𝜑 → (∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓 ∈ 𝑎 ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
60	3	inex1 5277	. . . . . . 7 ⊢ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ∈ V
61	60	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ∈ V)
62	13	sselda 3931	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → 𝑓 ∈ 𝐴)
63		fnwe2.su	. . . . . . . . . 10 ⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈)
64		fnwe2.t	. . . . . . . . . 10 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))}
65		fnwe2.s	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑈 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑥)})
66	63, 64, 65	fnwe2lem1 44036	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
67		wefr 5641	. . . . . . . . 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 4183	. . . . . . 7 ⊢ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ⊆ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}
72	71	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ⊆ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
73		simprl 783	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → 𝑓 ∈ 𝑎)
74		fveqeq2 6892	. . . . . . . . 9 ⊢ (𝑦 = 𝑓 → ((𝐹‘𝑦) = (𝐹‘𝑓) ↔ (𝐹‘𝑓) = (𝐹‘𝑓)))
75	62	adantrr 730	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → 𝑓 ∈ 𝐴)
76		eqidd 2762	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝐹‘𝑓) = (𝐹‘𝑓))
77	74, 75, 76	elrabd 3647	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → 𝑓 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
78	73, 77	elind 4146	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → 𝑓 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}))
79	78	ne0d 4288	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ≠ ∅)
80		fri 5609	. . . . . 6 ⊢ ((((𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ∈ V ∧ ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 Fr {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ∧ ((𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ⊆ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)} ∧ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ≠ ∅)) → ∃𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)
81	61, 70, 72, 79, 80	syl22anc 852	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → ∃𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)
82		elin 3915	. . . . . . . 8 ⊢ (𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑒 ∈ 𝑎 ∧ 𝑒 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}))
83		fveqeq2 6892	. . . . . . . . . 10 ⊢ (𝑦 = 𝑒 → ((𝐹‘𝑦) = (𝐹‘𝑓) ↔ (𝐹‘𝑒) = (𝐹‘𝑓)))
84	83	elrab 3645	. . . . . . . . 9 ⊢ (𝑒 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)} ↔ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))
85	84	anbi2i 635	. . . . . . . 8 ⊢ ((𝑒 ∈ 𝑎 ∧ 𝑒 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓))))
86	82, 85	bitri 278	. . . . . . 7 ⊢ (𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓))))
87		elin 3915	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑔 ∈ 𝑎 ∧ 𝑔 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}))
88		fveqeq2 6892	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑔 → ((𝐹‘𝑦) = (𝐹‘𝑓) ↔ (𝐹‘𝑔) = (𝐹‘𝑓)))
89	88	elrab 3645	. . . . . . . . . . . . . 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 3105	. . . . . . . . 9 ⊢ (∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 ↔ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))
96		simplrl 789	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) → 𝑒 ∈ 𝑎)
97		fveq2 6883	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑐 → (𝐹‘𝑑) = (𝐹‘𝑐))
98	97	breq1d 5113	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑐 → ((𝐹‘𝑑)𝑅(𝐹‘𝑓) ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑓)))
99	98	notbid 321	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑐 → (¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓) ↔ ¬ (𝐹‘𝑐)𝑅(𝐹‘𝑓)))
100		simplrr 790	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) → ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))
101	100	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))
102		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → 𝑐 ∈ 𝑎)
103	99, 101, 102	rspcdva 3578	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ (𝐹‘𝑐)𝑅(𝐹‘𝑓))
104		simprrr 794	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) → (𝐹‘𝑒) = (𝐹‘𝑓))
105	104	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → (𝐹‘𝑒) = (𝐹‘𝑓))
106	105	breq2d 5115	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ((𝐹‘𝑐)𝑅(𝐹‘𝑒) ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑓)))
107	103, 106	mtbird 328	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ (𝐹‘𝑐)𝑅(𝐹‘𝑒))
108	13	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) → 𝑎 ⊆ 𝐴)
109	108	sselda 3931	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → 𝑐 ∈ 𝐴)
110	109	adantrr 730	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → 𝑐 ∈ 𝐴)
111		simprr 785	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝐹‘𝑐) = (𝐹‘𝑒))
112	104	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝐹‘𝑒) = (𝐹‘𝑓))
113	111, 112	eqtrd 2796	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝐹‘𝑐) = (𝐹‘𝑓))
114		eleq1w 2844	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑐 → (𝑔 ∈ 𝐴 ↔ 𝑐 ∈ 𝐴))
115		fveqeq2 6892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑐 → ((𝐹‘𝑔) = (𝐹‘𝑓) ↔ (𝐹‘𝑐) = (𝐹‘𝑓)))
116	114, 115	anbi12d 644	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑐 → ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) ↔ (𝑐 ∈ 𝐴 ∧ (𝐹‘𝑐) = (𝐹‘𝑓))))
117		breq1 5106	. . . . . . . . . . . . . . . . . . . . 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 3578	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ((𝑐 ∈ 𝐴 ∧ (𝐹‘𝑐) = (𝐹‘𝑓)) → ¬ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))
123	110, 113, 122	mp2and 712	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ¬ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)
124	111, 112	eqtr2d 2797	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝐹‘𝑓) = (𝐹‘𝑐))
125	124	csbeq1d 3851	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 = ⦋(𝐹‘𝑐) / 𝑧⦌𝑆)
126	125	breqd 5114	. . . . . . . . . . . . . . . . 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 44035	. . . . . . . . . . . . 13 ⊢ (𝑐𝑇𝑒 ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑒) ∨ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒)))
134	132, 133	sylnibr 332	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ 𝑐𝑇𝑒)
135	134	ralrimiva 3155	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) → ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑒)
136		breq2 5107	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑒 → (𝑐𝑇𝑏 ↔ 𝑐𝑇𝑒))
137	136	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑒 → (¬ 𝑐𝑇𝑏 ↔ ¬ 𝑐𝑇𝑒))
138	137	ralbidv 3186	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑒 → (∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏 ↔ ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑒))
139	138	rspcev 3577	. . . . . . . . . . 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 3162	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (∃𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏))
146	81, 145	mpd 16	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)
147	146	rexlimdvaa 3165	. . 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 2145   ≠ wne 2956  ∀wral 3077  ∃wrex 3087  {crab 3413  Vcvv 3451  ⦋csb 3847   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279   class class class wbr 5103  {copab 5167   Fr wfr 5601   We wwe 5603  dom cdm 5651  ran crn 5652   ↾ cres 5653   “ cima 5654  Fun wfun 6531   Fn wfn 6532  ⟶wf 6533  ‘cfv 6537

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545

This theorem is used by:  fnwe2  44039