Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fnwe2lem2 Structured version   Visualization version   GIF version

Theorem fnwe2lem2 36639
Description: Lemma for fnwe2 36641. 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.
StepHypRef Expression
1 fnwe2.f . . . 4 (𝜑 → (𝐹𝐴):𝐴𝐵)
2 ffun 5961 . . . 4 ((𝐹𝐴):𝐴𝐵 → Fun (𝐹𝐴))
3 vex 3176 . . . . 5 𝑎 ∈ V
43funimaex 5890 . . . 4 (Fun (𝐹𝐴) → ((𝐹𝐴) “ 𝑎) ∈ V)
51, 2, 43syl 18 . . 3 (𝜑 → ((𝐹𝐴) “ 𝑎) ∈ V)
6 fnwe2.r . . . 4 (𝜑𝑅 We 𝐵)
7 wefr 5028 . . . 4 (𝑅 We 𝐵𝑅 Fr 𝐵)
86, 7syl 17 . . 3 (𝜑𝑅 Fr 𝐵)
9 imassrn 5396 . . . 4 ((𝐹𝐴) “ 𝑎) ⊆ ran (𝐹𝐴)
10 frn 5966 . . . . 5 ((𝐹𝐴):𝐴𝐵 → ran (𝐹𝐴) ⊆ 𝐵)
111, 10syl 17 . . . 4 (𝜑 → ran (𝐹𝐴) ⊆ 𝐵)
129, 11syl5ss 3579 . . 3 (𝜑 → ((𝐹𝐴) “ 𝑎) ⊆ 𝐵)
13 incom 3767 . . . . . 6 (dom (𝐹𝐴) ∩ 𝑎) = (𝑎 ∩ dom (𝐹𝐴))
14 fnwe2lem2.a . . . . . . . 8 (𝜑𝑎𝐴)
15 fdm 5964 . . . . . . . . 9 ((𝐹𝐴):𝐴𝐵 → dom (𝐹𝐴) = 𝐴)
161, 15syl 17 . . . . . . . 8 (𝜑 → dom (𝐹𝐴) = 𝐴)
1714, 16sseqtr4d 3605 . . . . . . 7 (𝜑𝑎 ⊆ dom (𝐹𝐴))
18 df-ss 3554 . . . . . . 7 (𝑎 ⊆ dom (𝐹𝐴) ↔ (𝑎 ∩ dom (𝐹𝐴)) = 𝑎)
1917, 18sylib 207 . . . . . 6 (𝜑 → (𝑎 ∩ dom (𝐹𝐴)) = 𝑎)
2013, 19syl5eq 2656 . . . . 5 (𝜑 → (dom (𝐹𝐴) ∩ 𝑎) = 𝑎)
21 fnwe2lem2.n0 . . . . 5 (𝜑𝑎 ≠ ∅)
2220, 21eqnetrd 2849 . . . 4 (𝜑 → (dom (𝐹𝐴) ∩ 𝑎) ≠ ∅)
23 imadisj 5403 . . . . 5 (((𝐹𝐴) “ 𝑎) = ∅ ↔ (dom (𝐹𝐴) ∩ 𝑎) = ∅)
2423necon3bii 2834 . . . 4 (((𝐹𝐴) “ 𝑎) ≠ ∅ ↔ (dom (𝐹𝐴) ∩ 𝑎) ≠ ∅)
2522, 24sylibr 223 . . 3 (𝜑 → ((𝐹𝐴) “ 𝑎) ≠ ∅)
26 fri 5000 . . 3 (((((𝐹𝐴) “ 𝑎) ∈ V ∧ 𝑅 Fr 𝐵) ∧ (((𝐹𝐴) “ 𝑎) ⊆ 𝐵 ∧ ((𝐹𝐴) “ 𝑎) ≠ ∅)) → ∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
275, 8, 12, 25, 26syl22anc 1319 . 2 (𝜑 → ∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
28 df-ima 5051 . . . . . 6 ((𝐹𝐴) “ 𝑎) = ran ((𝐹𝐴) ↾ 𝑎)
2928rexeqi 3120 . . . . 5 (∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑑 ∈ ran ((𝐹𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
30 ffn 5958 . . . . . . . 8 ((𝐹𝐴):𝐴𝐵 → (𝐹𝐴) Fn 𝐴)
311, 30syl 17 . . . . . . 7 (𝜑 → (𝐹𝐴) Fn 𝐴)
32 fnssres 5918 . . . . . . 7 (((𝐹𝐴) Fn 𝐴𝑎𝐴) → ((𝐹𝐴) ↾ 𝑎) Fn 𝑎)
3331, 14, 32syl2anc 691 . . . . . 6 (𝜑 → ((𝐹𝐴) ↾ 𝑎) Fn 𝑎)
34 breq2 4587 . . . . . . . . 9 (𝑑 = (((𝐹𝐴) ↾ 𝑎)‘𝑓) → (𝑒𝑅𝑑𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3534notbid 307 . . . . . . . 8 (𝑑 = (((𝐹𝐴) ↾ 𝑎)‘𝑓) → (¬ 𝑒𝑅𝑑 ↔ ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3635ralbidv 2969 . . . . . . 7 (𝑑 = (((𝐹𝐴) ↾ 𝑎)‘𝑓) → (∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3736rexrn 6269 . . . . . 6 (((𝐹𝐴) ↾ 𝑎) Fn 𝑎 → (∃𝑑 ∈ ran ((𝐹𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓𝑎𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3833, 37syl 17 . . . . 5 (𝜑 → (∃𝑑 ∈ ran ((𝐹𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓𝑎𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3929, 38syl5bb 271 . . . 4 (𝜑 → (∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓𝑎𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4028raleqi 3119 . . . . . . . 8 (∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑒 ∈ ran ((𝐹𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓))
41 breq1 4586 . . . . . . . . . . 11 (𝑒 = (((𝐹𝐴) ↾ 𝑎)‘𝑑) → (𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4241notbid 307 . . . . . . . . . 10 (𝑒 = (((𝐹𝐴) ↾ 𝑎)‘𝑑) → (¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4342ralrn 6270 . . . . . . . . 9 (((𝐹𝐴) ↾ 𝑎) Fn 𝑎 → (∀𝑒 ∈ ran ((𝐹𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4433, 43syl 17 . . . . . . . 8 (𝜑 → (∀𝑒 ∈ ran ((𝐹𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4540, 44syl5bb 271 . . . . . . 7 (𝜑 → (∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4645adantr 480 . . . . . 6 ((𝜑𝑓𝑎) → (∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4714resabs1d 5348 . . . . . . . . . . . 12 (𝜑 → ((𝐹𝐴) ↾ 𝑎) = (𝐹𝑎))
4847ad2antrr 758 . . . . . . . . . . 11 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → ((𝐹𝐴) ↾ 𝑎) = (𝐹𝑎))
4948fveq1d 6105 . . . . . . . . . 10 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → (((𝐹𝐴) ↾ 𝑎)‘𝑑) = ((𝐹𝑎)‘𝑑))
50 fvres 6117 . . . . . . . . . . 11 (𝑑𝑎 → ((𝐹𝑎)‘𝑑) = (𝐹𝑑))
5150adantl 481 . . . . . . . . . 10 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → ((𝐹𝑎)‘𝑑) = (𝐹𝑑))
5249, 51eqtrd 2644 . . . . . . . . 9 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → (((𝐹𝐴) ↾ 𝑎)‘𝑑) = (𝐹𝑑))
5348fveq1d 6105 . . . . . . . . . 10 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → (((𝐹𝐴) ↾ 𝑎)‘𝑓) = ((𝐹𝑎)‘𝑓))
54 fvres 6117 . . . . . . . . . . 11 (𝑓𝑎 → ((𝐹𝑎)‘𝑓) = (𝐹𝑓))
5554ad2antlr 759 . . . . . . . . . 10 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → ((𝐹𝑎)‘𝑓) = (𝐹𝑓))
5653, 55eqtrd 2644 . . . . . . . . 9 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → (((𝐹𝐴) ↾ 𝑎)‘𝑓) = (𝐹𝑓))
5752, 56breq12d 4596 . . . . . . . 8 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → ((((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ (𝐹𝑑)𝑅(𝐹𝑓)))
5857notbid 307 . . . . . . 7 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → (¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ¬ (𝐹𝑑)𝑅(𝐹𝑓)))
5958ralbidva 2968 . . . . . 6 ((𝜑𝑓𝑎) → (∀𝑑𝑎 ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓)))
6046, 59bitrd 267 . . . . 5 ((𝜑𝑓𝑎) → (∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓)))
6160rexbidva 3031 . . . 4 (𝜑 → (∃𝑓𝑎𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∃𝑓𝑎𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓)))
6239, 61bitrd 267 . . 3 (𝜑 → (∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓𝑎𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓)))
633inex1 4727 . . . . . . 7 (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ∈ V
6463a1i 11 . . . . . 6 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ∈ V)
6514sselda 3568 . . . . . . . 8 ((𝜑𝑓𝑎) → 𝑓𝐴)
66 fnwe2.su . . . . . . . . . 10 (𝑧 = (𝐹𝑥) → 𝑆 = 𝑈)
67 fnwe2.t . . . . . . . . . 10 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝐹𝑥)𝑅(𝐹𝑦) ∨ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥𝑈𝑦))}
68 fnwe2.s . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝑈 We {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑥)})
6966, 67, 68fnwe2lem1 36638 . . . . . . . . 9 ((𝜑𝑓𝐴) → (𝐹𝑓) / 𝑧𝑆 We {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
70 wefr 5028 . . . . . . . . 9 ((𝐹𝑓) / 𝑧𝑆 We {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)} → (𝐹𝑓) / 𝑧𝑆 Fr {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
7169, 70syl 17 . . . . . . . 8 ((𝜑𝑓𝐴) → (𝐹𝑓) / 𝑧𝑆 Fr {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
7265, 71syldan 486 . . . . . . 7 ((𝜑𝑓𝑎) → (𝐹𝑓) / 𝑧𝑆 Fr {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
7372adantrr 749 . . . . . 6 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝐹𝑓) / 𝑧𝑆 Fr {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
74 inss2 3796 . . . . . . 7 (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ⊆ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}
7574a1i 11 . . . . . 6 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ⊆ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
76 simprl 790 . . . . . . . 8 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → 𝑓𝑎)
7765adantrr 749 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → 𝑓𝐴)
78 eqidd 2611 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝐹𝑓) = (𝐹𝑓))
79 fveq2 6103 . . . . . . . . . . 11 (𝑦 = 𝑓 → (𝐹𝑦) = (𝐹𝑓))
8079eqeq1d 2612 . . . . . . . . . 10 (𝑦 = 𝑓 → ((𝐹𝑦) = (𝐹𝑓) ↔ (𝐹𝑓) = (𝐹𝑓)))
8180elrab 3331 . . . . . . . . 9 (𝑓 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)} ↔ (𝑓𝐴 ∧ (𝐹𝑓) = (𝐹𝑓)))
8277, 78, 81sylanbrc 695 . . . . . . . 8 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → 𝑓 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
8376, 82elind 3760 . . . . . . 7 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → 𝑓 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}))
84 ne0i 3880 . . . . . . 7 (𝑓 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) → (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ≠ ∅)
8583, 84syl 17 . . . . . 6 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ≠ ∅)
86 fri 5000 . . . . . 6 ((((𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ∈ V ∧ (𝐹𝑓) / 𝑧𝑆 Fr {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ∧ ((𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ⊆ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)} ∧ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ≠ ∅)) → ∃𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)
8764, 73, 75, 85, 86syl22anc 1319 . . . . 5 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → ∃𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)
88 elin 3758 . . . . . . . 8 (𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑒𝑎𝑒 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}))
89 fveq2 6103 . . . . . . . . . . 11 (𝑦 = 𝑒 → (𝐹𝑦) = (𝐹𝑒))
9089eqeq1d 2612 . . . . . . . . . 10 (𝑦 = 𝑒 → ((𝐹𝑦) = (𝐹𝑓) ↔ (𝐹𝑒) = (𝐹𝑓)))
9190elrab 3331 . . . . . . . . 9 (𝑒 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)} ↔ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))
9291anbi2i 726 . . . . . . . 8 ((𝑒𝑎𝑒 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓))))
9388, 92bitri 263 . . . . . . 7 (𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓))))
94 elin 3758 . . . . . . . . . . . . 13 (𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑔𝑎𝑔 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}))
95 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑔 → (𝐹𝑦) = (𝐹𝑔))
9695eqeq1d 2612 . . . . . . . . . . . . . . 15 (𝑦 = 𝑔 → ((𝐹𝑦) = (𝐹𝑓) ↔ (𝐹𝑔) = (𝐹𝑓)))
9796elrab 3331 . . . . . . . . . . . . . 14 (𝑔 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)} ↔ (𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)))
9897anbi2i 726 . . . . . . . . . . . . 13 ((𝑔𝑎𝑔 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑔𝑎 ∧ (𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓))))
9994, 98bitri 263 . . . . . . . . . . . 12 (𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑔𝑎 ∧ (𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓))))
10099imbi1i 338 . . . . . . . . . . 11 ((𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒) ↔ ((𝑔𝑎 ∧ (𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓))) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒))
101 impexp 461 . . . . . . . . . . 11 (((𝑔𝑎 ∧ (𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓))) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒) ↔ (𝑔𝑎 → ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)))
102100, 101bitri 263 . . . . . . . . . 10 ((𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒) ↔ (𝑔𝑎 → ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)))
103102ralbii2 2961 . . . . . . . . 9 (∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 ↔ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒))
104 simplrl 796 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) → 𝑒𝑎)
105 simpr 476 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → 𝑐𝑎)
106 simplrr 797 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) → ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))
107106ad2antrr 758 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))
108 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑑 = 𝑐 → (𝐹𝑑) = (𝐹𝑐))
109108breq1d 4593 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑐 → ((𝐹𝑑)𝑅(𝐹𝑓) ↔ (𝐹𝑐)𝑅(𝐹𝑓)))
110109notbid 307 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑐 → (¬ (𝐹𝑑)𝑅(𝐹𝑓) ↔ ¬ (𝐹𝑐)𝑅(𝐹𝑓)))
111110rspcva 3280 . . . . . . . . . . . . . . . 16 ((𝑐𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓)) → ¬ (𝐹𝑐)𝑅(𝐹𝑓))
112105, 107, 111syl2anc 691 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ¬ (𝐹𝑐)𝑅(𝐹𝑓))
113 simprrr 801 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) → (𝐹𝑒) = (𝐹𝑓))
114113ad2antrr 758 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → (𝐹𝑒) = (𝐹𝑓))
115114breq2d 4595 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ((𝐹𝑐)𝑅(𝐹𝑒) ↔ (𝐹𝑐)𝑅(𝐹𝑓)))
116112, 115mtbird 314 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ¬ (𝐹𝑐)𝑅(𝐹𝑒))
11714ad3antrrr 762 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) → 𝑎𝐴)
118117sselda 3568 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → 𝑐𝐴)
119118adantrr 749 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → 𝑐𝐴)
120 simprr 792 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝐹𝑐) = (𝐹𝑒))
121113ad2antrr 758 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝐹𝑒) = (𝐹𝑓))
122120, 121eqtrd 2644 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝐹𝑐) = (𝐹𝑓))
123 simprl 790 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → 𝑐𝑎)
124 simplr 788 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒))
125 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝑐 → (𝑔𝐴𝑐𝐴))
126 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = 𝑐 → (𝐹𝑔) = (𝐹𝑐))
127126eqeq1d 2612 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝑐 → ((𝐹𝑔) = (𝐹𝑓) ↔ (𝐹𝑐) = (𝐹𝑓)))
128125, 127anbi12d 743 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑐 → ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) ↔ (𝑐𝐴 ∧ (𝐹𝑐) = (𝐹𝑓))))
129 breq1 4586 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝑐 → (𝑔(𝐹𝑓) / 𝑧𝑆𝑒𝑐(𝐹𝑓) / 𝑧𝑆𝑒))
130129notbid 307 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑐 → (¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 ↔ ¬ 𝑐(𝐹𝑓) / 𝑧𝑆𝑒))
131128, 130imbi12d 333 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑐 → (((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒) ↔ ((𝑐𝐴 ∧ (𝐹𝑐) = (𝐹𝑓)) → ¬ 𝑐(𝐹𝑓) / 𝑧𝑆𝑒)))
132131rspcva 3280 . . . . . . . . . . . . . . . . . . 19 ((𝑐𝑎 ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) → ((𝑐𝐴 ∧ (𝐹𝑐) = (𝐹𝑓)) → ¬ 𝑐(𝐹𝑓) / 𝑧𝑆𝑒))
133123, 124, 132syl2anc 691 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → ((𝑐𝐴 ∧ (𝐹𝑐) = (𝐹𝑓)) → ¬ 𝑐(𝐹𝑓) / 𝑧𝑆𝑒))
134119, 122, 133mp2and 711 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → ¬ 𝑐(𝐹𝑓) / 𝑧𝑆𝑒)
135120, 121eqtr2d 2645 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝐹𝑓) = (𝐹𝑐))
136135csbeq1d 3506 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝐹𝑓) / 𝑧𝑆 = (𝐹𝑐) / 𝑧𝑆)
137136breqd 4594 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝑐(𝐹𝑓) / 𝑧𝑆𝑒𝑐(𝐹𝑐) / 𝑧𝑆𝑒))
138134, 137mtbid 313 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → ¬ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒)
139138expr 641 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ((𝐹𝑐) = (𝐹𝑒) → ¬ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒))
140 imnan 437 . . . . . . . . . . . . . . 15 (((𝐹𝑐) = (𝐹𝑒) → ¬ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒) ↔ ¬ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒))
141139, 140sylib 207 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ¬ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒))
142 ioran 510 . . . . . . . . . . . . . 14 (¬ ((𝐹𝑐)𝑅(𝐹𝑒) ∨ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒)) ↔ (¬ (𝐹𝑐)𝑅(𝐹𝑒) ∧ ¬ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒)))
143116, 141, 142sylanbrc 695 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ¬ ((𝐹𝑐)𝑅(𝐹𝑒) ∨ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒)))
14466, 67fnwe2val 36637 . . . . . . . . . . . . 13 (𝑐𝑇𝑒 ↔ ((𝐹𝑐)𝑅(𝐹𝑒) ∨ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒)))
145143, 144sylnibr 318 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ¬ 𝑐𝑇𝑒)
146145ralrimiva 2949 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) → ∀𝑐𝑎 ¬ 𝑐𝑇𝑒)
147 breq2 4587 . . . . . . . . . . . . . 14 (𝑏 = 𝑒 → (𝑐𝑇𝑏𝑐𝑇𝑒))
148147notbid 307 . . . . . . . . . . . . 13 (𝑏 = 𝑒 → (¬ 𝑐𝑇𝑏 ↔ ¬ 𝑐𝑇𝑒))
149148ralbidv 2969 . . . . . . . . . . . 12 (𝑏 = 𝑒 → (∀𝑐𝑎 ¬ 𝑐𝑇𝑏 ↔ ∀𝑐𝑎 ¬ 𝑐𝑇𝑒))
150149rspcev 3282 . . . . . . . . . . 11 ((𝑒𝑎 ∧ ∀𝑐𝑎 ¬ 𝑐𝑇𝑒) → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)
151104, 146, 150syl2anc 691 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)
152151ex 449 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) → (∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒) → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏))
153103, 152syl5bi 231 . . . . . . . 8 (((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) → (∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏))
154153ex 449 . . . . . . 7 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → ((𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓))) → (∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)))
15593, 154syl5bi 231 . . . . . 6 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) → (∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)))
156155rexlimdv 3012 . . . . 5 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (∃𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏))
15787, 156mpd 15 . . . 4 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)
158157rexlimdvaa 3014 . . 3 (𝜑 → (∃𝑓𝑎𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓) → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏))
15962, 158sylbid 229 . 2 (𝜑 → (∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏))
16027, 159mpd 15 1 (𝜑 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wo 382  wa 383   = wceq 1475  wcel 1977  wne 2780  wral 2896  wrex 2897  {crab 2900  Vcvv 3173  csb 3499  cin 3539  wss 3540  c0 3874   class class class wbr 4583  {copab 4642   Fr wfr 4994   We wwe 4996  dom cdm 5038  ran crn 5039  cres 5040  cima 5041  Fun wfun 5798   Fn wfn 5799  wf 5800  cfv 5804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pr 4833
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812
This theorem is referenced by:  fnwe2  36641
  Copyright terms: Public domain W3C validator