Theorem fnwe2lem2 38230

Description: Lemma for fnwe2 38232. 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 6226	. . . 4 ⊢ ((𝐹 ↾ 𝐴):𝐴⟶𝐵 → Fun (𝐹 ↾ 𝐴))
3		vex 3353	. . . . 5 ⊢ 𝑎 ∈ V
4	3	funimaex 6154	. . . 4 ⊢ (Fun (𝐹 ↾ 𝐴) → ((𝐹 ↾ 𝐴) “ 𝑎) ∈ V)
5	1, 2, 4	3syl 18	. . 3 ⊢ (𝜑 → ((𝐹 ↾ 𝐴) “ 𝑎) ∈ V)
6		fnwe2.r	. . . 4 ⊢ (𝜑 → 𝑅 We 𝐵)
7		wefr 5267	. . . 4 ⊢ (𝑅 We 𝐵 → 𝑅 Fr 𝐵)
8	6, 7	syl 17	. . 3 ⊢ (𝜑 → 𝑅 Fr 𝐵)
9		imassrn 5659	. . . 4 ⊢ ((𝐹 ↾ 𝐴) “ 𝑎) ⊆ ran (𝐹 ↾ 𝐴)
10	1	frnd 6230	. . . 4 ⊢ (𝜑 → ran (𝐹 ↾ 𝐴) ⊆ 𝐵)
11	9, 10	syl5ss 3772	. . 3 ⊢ (𝜑 → ((𝐹 ↾ 𝐴) “ 𝑎) ⊆ 𝐵)
12		incom 3967	. . . . . 6 ⊢ (dom (𝐹 ↾ 𝐴) ∩ 𝑎) = (𝑎 ∩ dom (𝐹 ↾ 𝐴))
13		fnwe2lem2.a	. . . . . . . 8 ⊢ (𝜑 → 𝑎 ⊆ 𝐴)
14	1	fdmd 6232	. . . . . . . 8 ⊢ (𝜑 → dom (𝐹 ↾ 𝐴) = 𝐴)
15	13, 14	sseqtr4d 3802	. . . . . . 7 ⊢ (𝜑 → 𝑎 ⊆ dom (𝐹 ↾ 𝐴))
16		df-ss 3746	. . . . . . 7 ⊢ (𝑎 ⊆ dom (𝐹 ↾ 𝐴) ↔ (𝑎 ∩ dom (𝐹 ↾ 𝐴)) = 𝑎)
17	15, 16	sylib 209	. . . . . 6 ⊢ (𝜑 → (𝑎 ∩ dom (𝐹 ↾ 𝐴)) = 𝑎)
18	12, 17	syl5eq 2811	. . . . 5 ⊢ (𝜑 → (dom (𝐹 ↾ 𝐴) ∩ 𝑎) = 𝑎)
19		fnwe2lem2.n0	. . . . 5 ⊢ (𝜑 → 𝑎 ≠ ∅)
20	18, 19	eqnetrd 3004	. . . 4 ⊢ (𝜑 → (dom (𝐹 ↾ 𝐴) ∩ 𝑎) ≠ ∅)
21		imadisj 5666	. . . . 5 ⊢ (((𝐹 ↾ 𝐴) “ 𝑎) = ∅ ↔ (dom (𝐹 ↾ 𝐴) ∩ 𝑎) = ∅)
22	21	necon3bii 2989	. . . 4 ⊢ (((𝐹 ↾ 𝐴) “ 𝑎) ≠ ∅ ↔ (dom (𝐹 ↾ 𝐴) ∩ 𝑎) ≠ ∅)
23	20, 22	sylibr 225	. . 3 ⊢ (𝜑 → ((𝐹 ↾ 𝐴) “ 𝑎) ≠ ∅)
24		fri 5239	. . 3 ⊢ (((((𝐹 ↾ 𝐴) “ 𝑎) ∈ V ∧ 𝑅 Fr 𝐵) ∧ (((𝐹 ↾ 𝐴) “ 𝑎) ⊆ 𝐵 ∧ ((𝐹 ↾ 𝐴) “ 𝑎) ≠ ∅)) → ∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
25	5, 8, 11, 23, 24	syl22anc 867	. 2 ⊢ (𝜑 → ∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
26		df-ima 5290	. . . . . 6 ⊢ ((𝐹 ↾ 𝐴) “ 𝑎) = ran ((𝐹 ↾ 𝐴) ↾ 𝑎)
27	26	rexeqi 3291	. . . . 5 ⊢ (∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑑 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
28	1	ffnd 6224	. . . . . . 7 ⊢ (𝜑 → (𝐹 ↾ 𝐴) Fn 𝐴)
29		fnssres 6182	. . . . . . 7 ⊢ (((𝐹 ↾ 𝐴) Fn 𝐴 ∧ 𝑎 ⊆ 𝐴) → ((𝐹 ↾ 𝐴) ↾ 𝑎) Fn 𝑎)
30	28, 13, 29	syl2anc 579	. . . . . 6 ⊢ (𝜑 → ((𝐹 ↾ 𝐴) ↾ 𝑎) Fn 𝑎)
31		breq2 4813	. . . . . . . . 9 ⊢ (𝑑 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) → (𝑒𝑅𝑑 ↔ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
32	31	notbid 309	. . . . . . . 8 ⊢ (𝑑 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) → (¬ 𝑒𝑅𝑑 ↔ ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
33	32	ralbidv 3133	. . . . . . 7 ⊢ (𝑑 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) → (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
34	33	rexrn 6551	. . . . . 6 ⊢ (((𝐹 ↾ 𝐴) ↾ 𝑎) Fn 𝑎 → (∃𝑑 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓 ∈ 𝑎 ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
35	30, 34	syl 17	. . . . 5 ⊢ (𝜑 → (∃𝑑 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓 ∈ 𝑎 ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
36	27, 35	syl5bb 274	. . . 4 ⊢ (𝜑 → (∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓 ∈ 𝑎 ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
37	26	raleqi 3290	. . . . . . . 8 ⊢ (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑒 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓))
38		breq1 4812	. . . . . . . . . . 11 ⊢ (𝑒 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑) → (𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
39	38	notbid 309	. . . . . . . . . 10 ⊢ (𝑒 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑) → (¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
40	39	ralrn 6552	. . . . . . . . 9 ⊢ (((𝐹 ↾ 𝐴) ↾ 𝑎) Fn 𝑎 → (∀𝑒 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
41	30, 40	syl 17	. . . . . . . 8 ⊢ (𝜑 → (∀𝑒 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
42	37, 41	syl5bb 274	. . . . . . 7 ⊢ (𝜑 → (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
43	42	adantr 472	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)))
44	13	resabs1d 5603	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐹 ↾ 𝐴) ↾ 𝑎) = (𝐹 ↾ 𝑎))
45	44	ad2antrr 717	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → ((𝐹 ↾ 𝐴) ↾ 𝑎) = (𝐹 ↾ 𝑎))
46	45	fveq1d 6377	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑) = ((𝐹 ↾ 𝑎)‘𝑑))
47		fvres 6394	. . . . . . . . . . 11 ⊢ (𝑑 ∈ 𝑎 → ((𝐹 ↾ 𝑎)‘𝑑) = (𝐹‘𝑑))
48	47	adantl 473	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → ((𝐹 ↾ 𝑎)‘𝑑) = (𝐹‘𝑑))
49	46, 48	eqtrd 2799	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑) = (𝐹‘𝑑))
50	45	fveq1d 6377	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) = ((𝐹 ↾ 𝑎)‘𝑓))
51		fvres 6394	. . . . . . . . . . 11 ⊢ (𝑓 ∈ 𝑎 → ((𝐹 ↾ 𝑎)‘𝑓) = (𝐹‘𝑓))
52	51	ad2antlr 718	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → ((𝐹 ↾ 𝑎)‘𝑓) = (𝐹‘𝑓))
53	50, 52	eqtrd 2799	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) = (𝐹‘𝑓))
54	49, 53	breq12d 4822	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → ((((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
55	54	notbid 309	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
56	55	ralbidva 3132	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → (∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
57	43, 56	bitrd 270	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
58	57	rexbidva 3196	. . . 4 ⊢ (𝜑 → (∃𝑓 ∈ 𝑎 ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∃𝑓 ∈ 𝑎 ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
59	36, 58	bitrd 270	. . 3 ⊢ (𝜑 → (∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓 ∈ 𝑎 ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)))
60	3	inex1 4960	. . . . . . 7 ⊢ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ∈ V
61	60	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ∈ V)
62	13	sselda 3761	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → 𝑓 ∈ 𝐴)
63		fnwe2.su	. . . . . . . . . 10 ⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈)
64		fnwe2.t	. . . . . . . . . 10 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))}
65		fnwe2.s	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑈 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑥)})
66	63, 64, 65	fnwe2lem1 38229	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
67		wefr 5267	. . . . . . . . 9 ⊢ (⦋(𝐹‘𝑓) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)} → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 Fr {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
68	66, 67	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 Fr {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
69	62, 68	syldan 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 Fr {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
70	69	adantrr 708	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 Fr {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
71		inss2 3993	. . . . . . 7 ⊢ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ⊆ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}
72	71	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ⊆ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
73		simprl 787	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → 𝑓 ∈ 𝑎)
74	62	adantrr 708	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → 𝑓 ∈ 𝐴)
75		eqidd 2766	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝐹‘𝑓) = (𝐹‘𝑓))
76		fveqeq2 6384	. . . . . . . . . 10 ⊢ (𝑦 = 𝑓 → ((𝐹‘𝑦) = (𝐹‘𝑓) ↔ (𝐹‘𝑓) = (𝐹‘𝑓)))
77	76	elrab 3519	. . . . . . . . 9 ⊢ (𝑓 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)} ↔ (𝑓 ∈ 𝐴 ∧ (𝐹‘𝑓) = (𝐹‘𝑓)))
78	74, 75, 77	sylanbrc 578	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → 𝑓 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})
79	73, 78	elind 3960	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → 𝑓 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}))
80	79	ne0d 4086	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ≠ ∅)
81		fri 5239	. . . . . 6 ⊢ ((((𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ∈ V ∧ ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 Fr {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ∧ ((𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ⊆ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)} ∧ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ≠ ∅)) → ∃𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)
82	61, 70, 72, 80, 81	syl22anc 867	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → ∃𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)
83		elin 3958	. . . . . . . 8 ⊢ (𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑒 ∈ 𝑎 ∧ 𝑒 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}))
84		fveqeq2 6384	. . . . . . . . . 10 ⊢ (𝑦 = 𝑒 → ((𝐹‘𝑦) = (𝐹‘𝑓) ↔ (𝐹‘𝑒) = (𝐹‘𝑓)))
85	84	elrab 3519	. . . . . . . . 9 ⊢ (𝑒 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)} ↔ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))
86	85	anbi2i 616	. . . . . . . 8 ⊢ ((𝑒 ∈ 𝑎 ∧ 𝑒 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓))))
87	83, 86	bitri 266	. . . . . . 7 ⊢ (𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓))))
88		elin 3958	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑔 ∈ 𝑎 ∧ 𝑔 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}))
89		fveqeq2 6384	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑔 → ((𝐹‘𝑦) = (𝐹‘𝑓) ↔ (𝐹‘𝑔) = (𝐹‘𝑓)))
90	89	elrab 3519	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)} ↔ (𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)))
91	90	anbi2i 616	. . . . . . . . . . . . 13 ⊢ ((𝑔 ∈ 𝑎 ∧ 𝑔 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑔 ∈ 𝑎 ∧ (𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓))))
92	88, 91	bitri 266	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑔 ∈ 𝑎 ∧ (𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓))))
93	92	imbi1i 340	. . . . . . . . . . 11 ⊢ ((𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) ↔ ((𝑔 ∈ 𝑎 ∧ (𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓))) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))
94		impexp 441	. . . . . . . . . . 11 ⊢ (((𝑔 ∈ 𝑎 ∧ (𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓))) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) ↔ (𝑔 ∈ 𝑎 → ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)))
95	93, 94	bitri 266	. . . . . . . . . 10 ⊢ ((𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) ↔ (𝑔 ∈ 𝑎 → ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)))
96	95	ralbii2 3125	. . . . . . . . 9 ⊢ (∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 ↔ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))
97		simplrl 795	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) → 𝑒 ∈ 𝑎)
98		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → 𝑐 ∈ 𝑎)
99		simplrr 796	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) → ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))
100	99	ad2antrr 717	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))
101		fveq2 6375	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = 𝑐 → (𝐹‘𝑑) = (𝐹‘𝑐))
102	101	breq1d 4819	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑐 → ((𝐹‘𝑑)𝑅(𝐹‘𝑓) ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑓)))
103	102	notbid 309	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑐 → (¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓) ↔ ¬ (𝐹‘𝑐)𝑅(𝐹‘𝑓)))
104	103	rspcva 3459	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)) → ¬ (𝐹‘𝑐)𝑅(𝐹‘𝑓))
105	98, 100, 104	syl2anc 579	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ (𝐹‘𝑐)𝑅(𝐹‘𝑓))
106		simprrr 800	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) → (𝐹‘𝑒) = (𝐹‘𝑓))
107	106	ad2antrr 717	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → (𝐹‘𝑒) = (𝐹‘𝑓))
108	107	breq2d 4821	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ((𝐹‘𝑐)𝑅(𝐹‘𝑒) ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑓)))
109	105, 108	mtbird 316	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ (𝐹‘𝑐)𝑅(𝐹‘𝑒))
110	13	ad3antrrr 721	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) → 𝑎 ⊆ 𝐴)
111	110	sselda 3761	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → 𝑐 ∈ 𝐴)
112	111	adantrr 708	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → 𝑐 ∈ 𝐴)
113		simprr 789	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝐹‘𝑐) = (𝐹‘𝑒))
114	106	ad2antrr 717	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝐹‘𝑒) = (𝐹‘𝑓))
115	113, 114	eqtrd 2799	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝐹‘𝑐) = (𝐹‘𝑓))
116		simprl 787	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → 𝑐 ∈ 𝑎)
117		simplr 785	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))
118		eleq1w 2827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = 𝑐 → (𝑔 ∈ 𝐴 ↔ 𝑐 ∈ 𝐴))
119		fveqeq2 6384	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = 𝑐 → ((𝐹‘𝑔) = (𝐹‘𝑓) ↔ (𝐹‘𝑐) = (𝐹‘𝑓)))
120	118, 119	anbi12d 624	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑐 → ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) ↔ (𝑐 ∈ 𝐴 ∧ (𝐹‘𝑐) = (𝐹‘𝑓))))
121		breq1 4812	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = 𝑐 → (𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 ↔ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))
122	121	notbid 309	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑐 → (¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 ↔ ¬ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))
123	120, 122	imbi12d 335	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑐 → (((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) ↔ ((𝑐 ∈ 𝐴 ∧ (𝐹‘𝑐) = (𝐹‘𝑓)) → ¬ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)))
124	123	rspcva 3459	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 ∈ 𝑎 ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) → ((𝑐 ∈ 𝐴 ∧ (𝐹‘𝑐) = (𝐹‘𝑓)) → ¬ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))
125	116, 117, 124	syl2anc 579	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ((𝑐 ∈ 𝐴 ∧ (𝐹‘𝑐) = (𝐹‘𝑓)) → ¬ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))
126	112, 115, 125	mp2and 690	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ¬ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)
127	113, 114	eqtr2d 2800	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝐹‘𝑓) = (𝐹‘𝑐))
128	127	csbeq1d 3698	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 = ⦋(𝐹‘𝑐) / 𝑧⦌𝑆)
129	128	breqd 4820	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 ↔ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒))
130	126, 129	mtbid 315	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ¬ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒)
131	130	expr 448	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ((𝐹‘𝑐) = (𝐹‘𝑒) → ¬ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒))
132		imnan 388	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑐) = (𝐹‘𝑒) → ¬ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒) ↔ ¬ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒))
133	131, 132	sylib 209	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒))
134		ioran 1006	. . . . . . . . . . . . . 14 ⊢ (¬ ((𝐹‘𝑐)𝑅(𝐹‘𝑒) ∨ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒)) ↔ (¬ (𝐹‘𝑐)𝑅(𝐹‘𝑒) ∧ ¬ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒)))
135	109, 133, 134	sylanbrc 578	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ ((𝐹‘𝑐)𝑅(𝐹‘𝑒) ∨ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒)))
136	63, 64	fnwe2val 38228	. . . . . . . . . . . . 13 ⊢ (𝑐𝑇𝑒 ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑒) ∨ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒)))
137	135, 136	sylnibr 320	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ 𝑐𝑇𝑒)
138	137	ralrimiva 3113	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) → ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑒)
139		breq2 4813	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑒 → (𝑐𝑇𝑏 ↔ 𝑐𝑇𝑒))
140	139	notbid 309	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑒 → (¬ 𝑐𝑇𝑏 ↔ ¬ 𝑐𝑇𝑒))
141	140	ralbidv 3133	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑒 → (∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏 ↔ ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑒))
142	141	rspcev 3461	. . . . . . . . . . 11 ⊢ ((𝑒 ∈ 𝑎 ∧ ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑒) → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)
143	97, 138, 142	syl2anc 579	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)
144	143	ex 401	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) → (∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏))
145	96, 144	syl5bi 233	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) → (∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏))
146	145	ex 401	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → ((𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓))) → (∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)))
147	87, 146	syl5bi 233	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) → (∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)))
148	147	rexlimdv 3177	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (∃𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏))
149	82, 148	mpd 15	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)
150	149	rexlimdvaa 3179	. . 3 ⊢ (𝜑 → (∃𝑓 ∈ 𝑎 ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓) → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏))
151	59, 150	sylbid 231	. 2 ⊢ (𝜑 → (∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏))
152	25, 151	mpd 15	1 ⊢ (𝜑 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 197   ∧ wa 384   ∨ wo 873   = wceq 1652   ∈ wcel 2155   ≠ wne 2937  ∀wral 3055  ∃wrex 3056  {crab 3059  Vcvv 3350  ⦋csb 3691   ∩ cin 3731   ⊆ wss 3732  ∅c0 4079   class class class wbr 4809  {copab 4871   Fr wfr 5233   We wwe 5235  dom cdm 5277  ran crn 5278   ↾ cres 5279   “ cima 5280  Fun wfun 6062   Fn wfn 6063  ⟶wf 6064  ‘cfv 6068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pr 5062

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-fv 6076

This theorem is referenced by:  fnwe2  38232