Theorem fnwe2lem2 43040

Description: Lemma for fnwe2 43042. 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 6740	. . . 4 ⊢ ((𝐹 ↾ 𝐴):𝐴⟶𝐵 → Fun (𝐹 ↾ 𝐴))
3		vex 3482	. . . . 5 ⊢ 𝑎 ∈ V
4	3	funimaex 6656	. . . 4 ⊢ (Fun (𝐹 ↾ 𝐴) → ((𝐹 ↾ 𝐴) “ 𝑎) ∈ V)
5	1, 2, 4	3syl 18	. . 3 ⊢ (𝜑 → ((𝐹 ↾ 𝐴) “ 𝑎) ∈ V)
6		fnwe2.r	. . . 4 ⊢ (𝜑 → 𝑅 We 𝐵)
7		wefr 5679	. . . 4 ⊢ (𝑅 We 𝐵 → 𝑅 Fr 𝐵)
8	6, 7	syl 17	. . 3 ⊢ (𝜑 → 𝑅 Fr 𝐵)
9		imassrn 6091	. . . 4 ⊢ ((𝐹 ↾ 𝐴) “ 𝑎) ⊆ ran (𝐹 ↾ 𝐴)
10	1	frnd 6745	. . . 4 ⊢ (𝜑 → ran (𝐹 ↾ 𝐴) ⊆ 𝐵)
11	9, 10	sstrid 4007	. . 3 ⊢ (𝜑 → ((𝐹 ↾ 𝐴) “ 𝑎) ⊆ 𝐵)
12		incom 4217	. . . . . 6 ⊢ (dom (𝐹 ↾ 𝐴) ∩ 𝑎) = (𝑎 ∩ dom (𝐹 ↾ 𝐴))
13		fnwe2lem2.a	. . . . . . . 8 ⊢ (𝜑 → 𝑎 ⊆ 𝐴)
14	1	fdmd 6747	. . . . . . . 8 ⊢ (𝜑 → dom (𝐹 ↾ 𝐴) = 𝐴)
15	13, 14	sseqtrrd 4037	. . . . . . 7 ⊢ (𝜑 → 𝑎 ⊆ dom (𝐹 ↾ 𝐴))
16		dfss2 3981	. . . . . . 7 ⊢ (𝑎 ⊆ dom (𝐹 ↾ 𝐴) ↔ (𝑎 ∩ dom (𝐹 ↾ 𝐴)) = 𝑎)
17	15, 16	sylib 218	. . . . . 6 ⊢ (𝜑 → (𝑎 ∩ dom (𝐹 ↾ 𝐴)) = 𝑎)
18	12, 17	eqtrid 2787	. . . . 5 ⊢ (𝜑 → (dom (𝐹 ↾ 𝐴) ∩ 𝑎) = 𝑎)
19		fnwe2lem2.n0	. . . . 5 ⊢ (𝜑 → 𝑎 ≠ ∅)
20	18, 19	eqnetrd 3006	. . . 4 ⊢ (𝜑 → (dom (𝐹 ↾ 𝐴) ∩ 𝑎) ≠ ∅)
21		imadisj 6100	. . . . 5 ⊢ (((𝐹 ↾ 𝐴) “ 𝑎) = ∅ ↔ (dom (𝐹 ↾ 𝐴) ∩ 𝑎) = ∅)
22	21	necon3bii 2991	. . . 4 ⊢ (((𝐹 ↾ 𝐴) “ 𝑎) ≠ ∅ ↔ (dom (𝐹 ↾ 𝐴) ∩ 𝑎) ≠ ∅)
23	20, 22	sylibr 234	. . 3 ⊢ (𝜑 → ((𝐹 ↾ 𝐴) “ 𝑎) ≠ ∅)
24		fri 5646	. . 3 ⊢ (((((𝐹 ↾ 𝐴) “ 𝑎) ∈ V ∧ 𝑅 Fr 𝐵) ∧ (((𝐹 ↾ 𝐴) “ 𝑎) ⊆ 𝐵 ∧ ((𝐹 ↾ 𝐴) “ 𝑎) ≠ ∅)) → ∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
25	5, 8, 11, 23, 24	syl22anc 839	. 2 ⊢ (𝜑 → ∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
26		df-ima 5702	. . . . . 6 ⊢ ((𝐹 ↾ 𝐴) “ 𝑎) = ran ((𝐹 ↾ 𝐴) ↾ 𝑎)
27	26	rexeqi 3323	. . . . 5 ⊢ (∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑑 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
28	1	ffnd 6738	. . . . . . 7 ⊢ (𝜑 → (𝐹 ↾ 𝐴) Fn 𝐴)
29		fnssres 6692	. . . . . . 7 ⊢ (((𝐹 ↾ 𝐴) Fn 𝐴 ∧ 𝑎 ⊆ 𝐴) → ((𝐹 ↾ 𝐴) ↾ 𝑎) Fn 𝑎)
30	28, 13, 29	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((𝐹 ↾ 𝐴) ↾ 𝑎) Fn 𝑎)
31		breq2 5152	. . . . . . . . 9 ⊢ (𝑑 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) → (𝑒𝑅𝑑 ↔ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
32	31	notbid 318	. . . . . . . 8 ⊢ (𝑑 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) → (¬ 𝑒𝑅𝑑 ↔ ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
33	32	ralbidv 3176	. . . . . . 7 ⊢ (𝑑 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) → (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
34	33	rexrn 7107	. . . . . 6 ⊢ (((𝐹 ↾ 𝐴) ↾ 𝑎) Fn 𝑎 → (∃𝑑 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓 ∈ 𝑎 ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
35	30, 34	syl 17	. . . . 5 ⊢ (𝜑 → (∃𝑑 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓 ∈ 𝑎 ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
36	27, 35	bitrid 283	. . . 4 ⊢ (𝜑 → (∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓 ∈ 𝑎 ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
37	26	raleqi 3322	. . . . . . . 8 ⊢ (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑒 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓))
38		breq1 5151	. . . . . . . . . . 11 ⊢ (𝑒 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑) → (𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
39	38	notbid 318	. . . . . . . . . 10 ⊢ (𝑒 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑) → (¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
40	39	ralrn 7108	. . . . . . . . 9 ⊢ (((𝐹 ↾ 𝐴) ↾ 𝑎) Fn 𝑎 → (∀𝑒 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
41	30, 40	syl 17	. . . . . . . 8 ⊢ (𝜑 → (∀𝑒 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
42	37, 41	bitrid 283	. . . . . . 7 ⊢ (𝜑 → (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
43	42	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
44	13	resabs1d 6028	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐹 ↾ 𝐴) ↾ 𝑎) = (𝐹 ↾ 𝑎))
45	44	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → ((𝐹 ↾ 𝐴) ↾ 𝑎) = (𝐹 ↾ 𝑎))
46	45	fveq1d 6909	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑) = ((𝐹 ↾ 𝑎)‘𝑑))
47		fvres 6926	. . . . . . . . . . 11 ⊢ (𝑑 ∈ 𝑎 → ((𝐹 ↾ 𝑎)‘𝑑) = (𝐹‘𝑑))
48	47	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → ((𝐹 ↾ 𝑎)‘𝑑) = (𝐹‘𝑑))
49	46, 48	eqtrd 2775	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑) = (𝐹‘𝑑))
50	45	fveq1d 6909	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) = ((𝐹 ↾ 𝑎)‘𝑓))
51		fvres 6926	. . . . . . . . . . 11 ⊢ (𝑓 ∈ 𝑎 → ((𝐹 ↾ 𝑎)‘𝑓) = (𝐹‘𝑓))
52	51	ad2antlr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → ((𝐹 ↾ 𝑎)‘𝑓) = (𝐹‘𝑓))
53	50, 52	eqtrd 2775	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) = (𝐹‘𝑓))
54	49, 53	breq12d 5161	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → ((((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
55	54	notbid 318	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
56	55	ralbidva 3174	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → (∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
57	43, 56	bitrd 279	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
58	57	rexbidva 3175	. . . 4 ⊢ (𝜑 → (∃𝑓 ∈ 𝑎 ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∃𝑓 ∈ 𝑎 ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
59	36, 58	bitrd 279	. . 3 ⊢ (𝜑 → (∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓 ∈ 𝑎 ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
60	3	inex1 5323	. . . . . . 7 ⊢ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ∈ V
61	60	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ∈ V)
62	13	sselda 3995	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → 𝑓 ∈ 𝐴)
63		fnwe2.su	. . . . . . . . . 10 ⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈)
64		fnwe2.t	. . . . . . . . . 10 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))}
65		fnwe2.s	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑈 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑥)})
66	63, 64, 65	fnwe2lem1 43039	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
67		wefr 5679	. . . . . . . . 9 ⊢ (⦋(𝐹‘𝑓) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)} → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 Fr {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
68	66, 67	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 Fr {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
69	62, 68	syldan 591	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 Fr {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
70	69	adantrr 717	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 Fr {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
71		inss2 4246	. . . . . . 7 ⊢ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ⊆ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}
72	71	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ⊆ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
73		simprl 771	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → 𝑓 ∈ 𝑎)
74		fveqeq2 6916	. . . . . . . . 9 ⊢ (𝑦 = 𝑓 → ((𝐹‘𝑦) = (𝐹‘𝑓) ↔ (𝐹‘𝑓) = (𝐹‘𝑓)))
75	62	adantrr 717	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → 𝑓 ∈ 𝐴)
76		eqidd 2736	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝐹‘𝑓) = (𝐹‘𝑓))
77	74, 75, 76	elrabd 3697	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → 𝑓 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
78	73, 77	elind 4210	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → 𝑓 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}))
79	78	ne0d 4348	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ≠ ∅)
80		fri 5646	. . . . . 6 ⊢ ((((𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ∈ V ∧ ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 Fr {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ∧ ((𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ⊆ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)} ∧ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ≠ ∅)) → ∃𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)
81	61, 70, 72, 79, 80	syl22anc 839	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → ∃𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)
82		elin 3979	. . . . . . . 8 ⊢ (𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑒 ∈ 𝑎 ∧ 𝑒 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}))
83		fveqeq2 6916	. . . . . . . . . 10 ⊢ (𝑦 = 𝑒 → ((𝐹‘𝑦) = (𝐹‘𝑓) ↔ (𝐹‘𝑒) = (𝐹‘𝑓)))
84	83	elrab 3695	. . . . . . . . 9 ⊢ (𝑒 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)} ↔ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))
85	84	anbi2i 623	. . . . . . . 8 ⊢ ((𝑒 ∈ 𝑎 ∧ 𝑒 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓))))
86	82, 85	bitri 275	. . . . . . 7 ⊢ (𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓))))
87		elin 3979	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑔 ∈ 𝑎 ∧ 𝑔 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}))
88		fveqeq2 6916	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑔 → ((𝐹‘𝑦) = (𝐹‘𝑓) ↔ (𝐹‘𝑔) = (𝐹‘𝑓)))
89	88	elrab 3695	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)} ↔ (𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)))
90	89	anbi2i 623	. . . . . . . . . . . . 13 ⊢ ((𝑔 ∈ 𝑎 ∧ 𝑔 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑔 ∈ 𝑎 ∧ (𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓))))
91	87, 90	bitri 275	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑔 ∈ 𝑎 ∧ (𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓))))
92	91	imbi1i 349	. . . . . . . . . . 11 ⊢ ((𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) ↔ ((𝑔 ∈ 𝑎 ∧ (𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓))) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))
93		impexp 450	. . . . . . . . . . 11 ⊢ (((𝑔 ∈ 𝑎 ∧ (𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓))) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) ↔ (𝑔 ∈ 𝑎 → ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)))
94	92, 93	bitri 275	. . . . . . . . . 10 ⊢ ((𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) ↔ (𝑔 ∈ 𝑎 → ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)))
95	94	ralbii2 3087	. . . . . . . . 9 ⊢ (∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 ↔ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))
96		simplrl 777	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) → 𝑒 ∈ 𝑎)
97		fveq2 6907	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑐 → (𝐹‘𝑑) = (𝐹‘𝑐))
98	97	breq1d 5158	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑐 → ((𝐹‘𝑑)𝑅(𝐹‘𝑓) ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑓)))
99	98	notbid 318	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑐 → (¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓) ↔ ¬ (𝐹‘𝑐)𝑅(𝐹‘𝑓)))
100		simplrr 778	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) → ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))
101	100	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))
102		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → 𝑐 ∈ 𝑎)
103	99, 101, 102	rspcdva 3623	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ (𝐹‘𝑐)𝑅(𝐹‘𝑓))
104		simprrr 782	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) → (𝐹‘𝑒) = (𝐹‘𝑓))
105	104	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → (𝐹‘𝑒) = (𝐹‘𝑓))
106	105	breq2d 5160	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ((𝐹‘𝑐)𝑅(𝐹‘𝑒) ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑓)))
107	103, 106	mtbird 325	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ (𝐹‘𝑐)𝑅(𝐹‘𝑒))
108	13	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) → 𝑎 ⊆ 𝐴)
109	108	sselda 3995	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → 𝑐 ∈ 𝐴)
110	109	adantrr 717	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → 𝑐 ∈ 𝐴)
111		simprr 773	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝐹‘𝑐) = (𝐹‘𝑒))
112	104	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝐹‘𝑒) = (𝐹‘𝑓))
113	111, 112	eqtrd 2775	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝐹‘𝑐) = (𝐹‘𝑓))
114		eleq1w 2822	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑐 → (𝑔 ∈ 𝐴 ↔ 𝑐 ∈ 𝐴))
115		fveqeq2 6916	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑐 → ((𝐹‘𝑔) = (𝐹‘𝑓) ↔ (𝐹‘𝑐) = (𝐹‘𝑓)))
116	114, 115	anbi12d 632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑐 → ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) ↔ (𝑐 ∈ 𝐴 ∧ (𝐹‘𝑐) = (𝐹‘𝑓))))
117		breq1 5151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑐 → (𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 ↔ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))
118	117	notbid 318	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑐 → (¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 ↔ ¬ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))
119	116, 118	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑐 → (((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) ↔ ((𝑐 ∈ 𝐴 ∧ (𝐹‘𝑐) = (𝐹‘𝑓)) → ¬ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)))
120		simplr 769	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))
121		simprl 771	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → 𝑐 ∈ 𝑎)
122	119, 120, 121	rspcdva 3623	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ((𝑐 ∈ 𝐴 ∧ (𝐹‘𝑐) = (𝐹‘𝑓)) → ¬ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))
123	110, 113, 122	mp2and 699	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ¬ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)
124	111, 112	eqtr2d 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝐹‘𝑓) = (𝐹‘𝑐))
125	124	csbeq1d 3912	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 = ⦋(𝐹‘𝑐) / 𝑧⦌𝑆)
126	125	breqd 5159	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 ↔ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒))
127	123, 126	mtbid 324	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ¬ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒)
128	127	expr 456	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ((𝐹‘𝑐) = (𝐹‘𝑒) → ¬ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒))
129		imnan 399	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑐) = (𝐹‘𝑒) → ¬ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒) ↔ ¬ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒))
130	128, 129	sylib 218	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒))
131		ioran 985	. . . . . . . . . . . . . 14 ⊢ (¬ ((𝐹‘𝑐)𝑅(𝐹‘𝑒) ∨ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒)) ↔ (¬ (𝐹‘𝑐)𝑅(𝐹‘𝑒) ∧ ¬ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒)))
132	107, 130, 131	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ ((𝐹‘𝑐)𝑅(𝐹‘𝑒) ∨ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒)))
133	63, 64	fnwe2val 43038	. . . . . . . . . . . . 13 ⊢ (𝑐𝑇𝑒 ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑒) ∨ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒)))
134	132, 133	sylnibr 329	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ 𝑐𝑇𝑒)
135	134	ralrimiva 3144	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) → ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑒)
136		breq2 5152	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑒 → (𝑐𝑇𝑏 ↔ 𝑐𝑇𝑒))
137	136	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑒 → (¬ 𝑐𝑇𝑏 ↔ ¬ 𝑐𝑇𝑒))
138	137	ralbidv 3176	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑒 → (∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏 ↔ ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑒))
139	138	rspcev 3622	. . . . . . . . . . 11 ⊢ ((𝑒 ∈ 𝑎 ∧ ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑒) → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)
140	96, 135, 139	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)
141	140	ex 412	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) → (∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏))
142	95, 141	biimtrid 242	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) → (∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏))
143	142	ex 412	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → ((𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓))) → (∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)))
144	86, 143	biimtrid 242	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) → (∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)))
145	144	rexlimdv 3151	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (∃𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏))
146	81, 145	mpd 15	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)
147	146	rexlimdvaa 3154	. . 3 ⊢ (𝜑 → (∃𝑓 ∈ 𝑎 ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓) → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏))
148	59, 147	sylbid 240	. 2 ⊢ (𝜑 → (∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏))
149	25, 148	mpd 15	1 ⊢ (𝜑 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1537   ∈ wcel 2106   ≠ wne 2938  ∀wral 3059  ∃wrex 3068  {crab 3433  Vcvv 3478  ⦋csb 3908   ∩ cin 3962   ⊆ wss 3963  ∅c0 4339   class class class wbr 5148  {copab 5210   Fr wfr 5638   We wwe 5640  dom cdm 5689  ran crn 5690   ↾ cres 5691   “ cima 5692  Fun wfun 6557   Fn wfn 6558  ⟶wf 6559  ‘cfv 6563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-fv 6571

This theorem is referenced by:  fnwe2  43042