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 37938
Description: Lemma for fnwe2 37940. 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 6086 . . . 4 ((𝐹𝐴):𝐴𝐵 → Fun (𝐹𝐴))
3 vex 3234 . . . . 5 𝑎 ∈ V
43funimaex 6014 . . . 4 (Fun (𝐹𝐴) → ((𝐹𝐴) “ 𝑎) ∈ V)
51, 2, 43syl 18 . . 3 (𝜑 → ((𝐹𝐴) “ 𝑎) ∈ V)
6 fnwe2.r . . . 4 (𝜑𝑅 We 𝐵)
7 wefr 5133 . . . 4 (𝑅 We 𝐵𝑅 Fr 𝐵)
86, 7syl 17 . . 3 (𝜑𝑅 Fr 𝐵)
9 imassrn 5512 . . . 4 ((𝐹𝐴) “ 𝑎) ⊆ ran (𝐹𝐴)
10 frn 6091 . . . . 5 ((𝐹𝐴):𝐴𝐵 → ran (𝐹𝐴) ⊆ 𝐵)
111, 10syl 17 . . . 4 (𝜑 → ran (𝐹𝐴) ⊆ 𝐵)
129, 11syl5ss 3647 . . 3 (𝜑 → ((𝐹𝐴) “ 𝑎) ⊆ 𝐵)
13 incom 3838 . . . . . 6 (dom (𝐹𝐴) ∩ 𝑎) = (𝑎 ∩ dom (𝐹𝐴))
14 fnwe2lem2.a . . . . . . . 8 (𝜑𝑎𝐴)
15 fdm 6089 . . . . . . . . 9 ((𝐹𝐴):𝐴𝐵 → dom (𝐹𝐴) = 𝐴)
161, 15syl 17 . . . . . . . 8 (𝜑 → dom (𝐹𝐴) = 𝐴)
1714, 16sseqtr4d 3675 . . . . . . 7 (𝜑𝑎 ⊆ dom (𝐹𝐴))
18 df-ss 3621 . . . . . . 7 (𝑎 ⊆ dom (𝐹𝐴) ↔ (𝑎 ∩ dom (𝐹𝐴)) = 𝑎)
1917, 18sylib 208 . . . . . 6 (𝜑 → (𝑎 ∩ dom (𝐹𝐴)) = 𝑎)
2013, 19syl5eq 2697 . . . . 5 (𝜑 → (dom (𝐹𝐴) ∩ 𝑎) = 𝑎)
21 fnwe2lem2.n0 . . . . 5 (𝜑𝑎 ≠ ∅)
2220, 21eqnetrd 2890 . . . 4 (𝜑 → (dom (𝐹𝐴) ∩ 𝑎) ≠ ∅)
23 imadisj 5519 . . . . 5 (((𝐹𝐴) “ 𝑎) = ∅ ↔ (dom (𝐹𝐴) ∩ 𝑎) = ∅)
2423necon3bii 2875 . . . 4 (((𝐹𝐴) “ 𝑎) ≠ ∅ ↔ (dom (𝐹𝐴) ∩ 𝑎) ≠ ∅)
2522, 24sylibr 224 . . 3 (𝜑 → ((𝐹𝐴) “ 𝑎) ≠ ∅)
26 fri 5105 . . 3 (((((𝐹𝐴) “ 𝑎) ∈ V ∧ 𝑅 Fr 𝐵) ∧ (((𝐹𝐴) “ 𝑎) ⊆ 𝐵 ∧ ((𝐹𝐴) “ 𝑎) ≠ ∅)) → ∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
275, 8, 12, 25, 26syl22anc 1367 . 2 (𝜑 → ∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
28 df-ima 5156 . . . . . 6 ((𝐹𝐴) “ 𝑎) = ran ((𝐹𝐴) ↾ 𝑎)
2928rexeqi 3173 . . . . 5 (∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑑 ∈ ran ((𝐹𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
30 ffn 6083 . . . . . . . 8 ((𝐹𝐴):𝐴𝐵 → (𝐹𝐴) Fn 𝐴)
311, 30syl 17 . . . . . . 7 (𝜑 → (𝐹𝐴) Fn 𝐴)
32 fnssres 6042 . . . . . . 7 (((𝐹𝐴) Fn 𝐴𝑎𝐴) → ((𝐹𝐴) ↾ 𝑎) Fn 𝑎)
3331, 14, 32syl2anc 694 . . . . . 6 (𝜑 → ((𝐹𝐴) ↾ 𝑎) Fn 𝑎)
34 breq2 4689 . . . . . . . . 9 (𝑑 = (((𝐹𝐴) ↾ 𝑎)‘𝑓) → (𝑒𝑅𝑑𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3534notbid 307 . . . . . . . 8 (𝑑 = (((𝐹𝐴) ↾ 𝑎)‘𝑓) → (¬ 𝑒𝑅𝑑 ↔ ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3635ralbidv 3015 . . . . . . 7 (𝑑 = (((𝐹𝐴) ↾ 𝑎)‘𝑓) → (∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3736rexrn 6401 . . . . . 6 (((𝐹𝐴) ↾ 𝑎) Fn 𝑎 → (∃𝑑 ∈ ran ((𝐹𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓𝑎𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3833, 37syl 17 . . . . 5 (𝜑 → (∃𝑑 ∈ ran ((𝐹𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓𝑎𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3929, 38syl5bb 272 . . . 4 (𝜑 → (∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓𝑎𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4028raleqi 3172 . . . . . . . 8 (∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑒 ∈ ran ((𝐹𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓))
41 breq1 4688 . . . . . . . . . . 11 (𝑒 = (((𝐹𝐴) ↾ 𝑎)‘𝑑) → (𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4241notbid 307 . . . . . . . . . 10 (𝑒 = (((𝐹𝐴) ↾ 𝑎)‘𝑑) → (¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4342ralrn 6402 . . . . . . . . 9 (((𝐹𝐴) ↾ 𝑎) Fn 𝑎 → (∀𝑒 ∈ ran ((𝐹𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4433, 43syl 17 . . . . . . . 8 (𝜑 → (∀𝑒 ∈ ran ((𝐹𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4540, 44syl5bb 272 . . . . . . 7 (𝜑 → (∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4645adantr 480 . . . . . 6 ((𝜑𝑓𝑎) → (∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4714resabs1d 5463 . . . . . . . . . . . 12 (𝜑 → ((𝐹𝐴) ↾ 𝑎) = (𝐹𝑎))
4847ad2antrr 762 . . . . . . . . . . 11 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → ((𝐹𝐴) ↾ 𝑎) = (𝐹𝑎))
4948fveq1d 6231 . . . . . . . . . 10 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → (((𝐹𝐴) ↾ 𝑎)‘𝑑) = ((𝐹𝑎)‘𝑑))
50 fvres 6245 . . . . . . . . . . 11 (𝑑𝑎 → ((𝐹𝑎)‘𝑑) = (𝐹𝑑))
5150adantl 481 . . . . . . . . . 10 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → ((𝐹𝑎)‘𝑑) = (𝐹𝑑))
5249, 51eqtrd 2685 . . . . . . . . 9 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → (((𝐹𝐴) ↾ 𝑎)‘𝑑) = (𝐹𝑑))
5348fveq1d 6231 . . . . . . . . . 10 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → (((𝐹𝐴) ↾ 𝑎)‘𝑓) = ((𝐹𝑎)‘𝑓))
54 fvres 6245 . . . . . . . . . . 11 (𝑓𝑎 → ((𝐹𝑎)‘𝑓) = (𝐹𝑓))
5554ad2antlr 763 . . . . . . . . . 10 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → ((𝐹𝑎)‘𝑓) = (𝐹𝑓))
5653, 55eqtrd 2685 . . . . . . . . 9 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → (((𝐹𝐴) ↾ 𝑎)‘𝑓) = (𝐹𝑓))
5752, 56breq12d 4698 . . . . . . . 8 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → ((((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ (𝐹𝑑)𝑅(𝐹𝑓)))
5857notbid 307 . . . . . . 7 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → (¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ¬ (𝐹𝑑)𝑅(𝐹𝑓)))
5958ralbidva 3014 . . . . . 6 ((𝜑𝑓𝑎) → (∀𝑑𝑎 ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓)))
6046, 59bitrd 268 . . . . 5 ((𝜑𝑓𝑎) → (∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓)))
6160rexbidva 3078 . . . 4 (𝜑 → (∃𝑓𝑎𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∃𝑓𝑎𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓)))
6239, 61bitrd 268 . . 3 (𝜑 → (∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓𝑎𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓)))
633inex1 4832 . . . . . . 7 (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ∈ V
6463a1i 11 . . . . . 6 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ∈ V)
6514sselda 3636 . . . . . . . 8 ((𝜑𝑓𝑎) → 𝑓𝐴)
66 fnwe2.su . . . . . . . . . 10 (𝑧 = (𝐹𝑥) → 𝑆 = 𝑈)
67 fnwe2.t . . . . . . . . . 10 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝐹𝑥)𝑅(𝐹𝑦) ∨ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥𝑈𝑦))}
68 fnwe2.s . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝑈 We {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑥)})
6966, 67, 68fnwe2lem1 37937 . . . . . . . . 9 ((𝜑𝑓𝐴) → (𝐹𝑓) / 𝑧𝑆 We {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
70 wefr 5133 . . . . . . . . 9 ((𝐹𝑓) / 𝑧𝑆 We {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)} → (𝐹𝑓) / 𝑧𝑆 Fr {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
7169, 70syl 17 . . . . . . . 8 ((𝜑𝑓𝐴) → (𝐹𝑓) / 𝑧𝑆 Fr {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
7265, 71syldan 486 . . . . . . 7 ((𝜑𝑓𝑎) → (𝐹𝑓) / 𝑧𝑆 Fr {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
7372adantrr 753 . . . . . 6 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝐹𝑓) / 𝑧𝑆 Fr {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
74 inss2 3867 . . . . . . 7 (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ⊆ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}
7574a1i 11 . . . . . 6 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ⊆ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
76 simprl 809 . . . . . . . 8 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → 𝑓𝑎)
7765adantrr 753 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → 𝑓𝐴)
78 eqidd 2652 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝐹𝑓) = (𝐹𝑓))
79 fveq2 6229 . . . . . . . . . . 11 (𝑦 = 𝑓 → (𝐹𝑦) = (𝐹𝑓))
8079eqeq1d 2653 . . . . . . . . . 10 (𝑦 = 𝑓 → ((𝐹𝑦) = (𝐹𝑓) ↔ (𝐹𝑓) = (𝐹𝑓)))
8180elrab 3396 . . . . . . . . 9 (𝑓 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)} ↔ (𝑓𝐴 ∧ (𝐹𝑓) = (𝐹𝑓)))
8277, 78, 81sylanbrc 699 . . . . . . . 8 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → 𝑓 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
8376, 82elind 3831 . . . . . . 7 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → 𝑓 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}))
84 ne0i 3954 . . . . . . 7 (𝑓 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) → (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ≠ ∅)
8583, 84syl 17 . . . . . 6 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ≠ ∅)
86 fri 5105 . . . . . 6 ((((𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ∈ V ∧ (𝐹𝑓) / 𝑧𝑆 Fr {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ∧ ((𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ⊆ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)} ∧ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ≠ ∅)) → ∃𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)
8764, 73, 75, 85, 86syl22anc 1367 . . . . 5 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → ∃𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)
88 elin 3829 . . . . . . . 8 (𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑒𝑎𝑒 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}))
89 fveq2 6229 . . . . . . . . . . 11 (𝑦 = 𝑒 → (𝐹𝑦) = (𝐹𝑒))
9089eqeq1d 2653 . . . . . . . . . 10 (𝑦 = 𝑒 → ((𝐹𝑦) = (𝐹𝑓) ↔ (𝐹𝑒) = (𝐹𝑓)))
9190elrab 3396 . . . . . . . . 9 (𝑒 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)} ↔ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))
9291anbi2i 730 . . . . . . . 8 ((𝑒𝑎𝑒 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓))))
9388, 92bitri 264 . . . . . . 7 (𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓))))
94 elin 3829 . . . . . . . . . . . . 13 (𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑔𝑎𝑔 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}))
95 fveq2 6229 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑔 → (𝐹𝑦) = (𝐹𝑔))
9695eqeq1d 2653 . . . . . . . . . . . . . . 15 (𝑦 = 𝑔 → ((𝐹𝑦) = (𝐹𝑓) ↔ (𝐹𝑔) = (𝐹𝑓)))
9796elrab 3396 . . . . . . . . . . . . . 14 (𝑔 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)} ↔ (𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)))
9897anbi2i 730 . . . . . . . . . . . . 13 ((𝑔𝑎𝑔 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑔𝑎 ∧ (𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓))))
9994, 98bitri 264 . . . . . . . . . . . 12 (𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑔𝑎 ∧ (𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓))))
10099imbi1i 338 . . . . . . . . . . 11 ((𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒) ↔ ((𝑔𝑎 ∧ (𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓))) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒))
101 impexp 461 . . . . . . . . . . 11 (((𝑔𝑎 ∧ (𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓))) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒) ↔ (𝑔𝑎 → ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)))
102100, 101bitri 264 . . . . . . . . . 10 ((𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒) ↔ (𝑔𝑎 → ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)))
103102ralbii2 3007 . . . . . . . . 9 (∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 ↔ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒))
104 simplrl 817 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) → 𝑒𝑎)
105 simpr 476 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → 𝑐𝑎)
106 simplrr 818 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) → ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))
107106ad2antrr 762 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))
108 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑑 = 𝑐 → (𝐹𝑑) = (𝐹𝑐))
109108breq1d 4695 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑐 → ((𝐹𝑑)𝑅(𝐹𝑓) ↔ (𝐹𝑐)𝑅(𝐹𝑓)))
110109notbid 307 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑐 → (¬ (𝐹𝑑)𝑅(𝐹𝑓) ↔ ¬ (𝐹𝑐)𝑅(𝐹𝑓)))
111110rspcva 3338 . . . . . . . . . . . . . . . 16 ((𝑐𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓)) → ¬ (𝐹𝑐)𝑅(𝐹𝑓))
112105, 107, 111syl2anc 694 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ¬ (𝐹𝑐)𝑅(𝐹𝑓))
113 simprrr 822 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) → (𝐹𝑒) = (𝐹𝑓))
114113ad2antrr 762 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → (𝐹𝑒) = (𝐹𝑓))
115114breq2d 4697 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ((𝐹𝑐)𝑅(𝐹𝑒) ↔ (𝐹𝑐)𝑅(𝐹𝑓)))
116112, 115mtbird 314 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ¬ (𝐹𝑐)𝑅(𝐹𝑒))
11714ad3antrrr 766 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) → 𝑎𝐴)
118117sselda 3636 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → 𝑐𝐴)
119118adantrr 753 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → 𝑐𝐴)
120 simprr 811 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝐹𝑐) = (𝐹𝑒))
121113ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝐹𝑒) = (𝐹𝑓))
122120, 121eqtrd 2685 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝐹𝑐) = (𝐹𝑓))
123 simprl 809 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → 𝑐𝑎)
124 simplr 807 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒))
125 eleq1 2718 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝑐 → (𝑔𝐴𝑐𝐴))
126 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = 𝑐 → (𝐹𝑔) = (𝐹𝑐))
127126eqeq1d 2653 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝑐 → ((𝐹𝑔) = (𝐹𝑓) ↔ (𝐹𝑐) = (𝐹𝑓)))
128125, 127anbi12d 747 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑐 → ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) ↔ (𝑐𝐴 ∧ (𝐹𝑐) = (𝐹𝑓))))
129 breq1 4688 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝑐 → (𝑔(𝐹𝑓) / 𝑧𝑆𝑒𝑐(𝐹𝑓) / 𝑧𝑆𝑒))
130129notbid 307 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑐 → (¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 ↔ ¬ 𝑐(𝐹𝑓) / 𝑧𝑆𝑒))
131128, 130imbi12d 333 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑐 → (((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒) ↔ ((𝑐𝐴 ∧ (𝐹𝑐) = (𝐹𝑓)) → ¬ 𝑐(𝐹𝑓) / 𝑧𝑆𝑒)))
132131rspcva 3338 . . . . . . . . . . . . . . . . . . 19 ((𝑐𝑎 ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) → ((𝑐𝐴 ∧ (𝐹𝑐) = (𝐹𝑓)) → ¬ 𝑐(𝐹𝑓) / 𝑧𝑆𝑒))
133123, 124, 132syl2anc 694 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → ((𝑐𝐴 ∧ (𝐹𝑐) = (𝐹𝑓)) → ¬ 𝑐(𝐹𝑓) / 𝑧𝑆𝑒))
134119, 122, 133mp2and 715 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → ¬ 𝑐(𝐹𝑓) / 𝑧𝑆𝑒)
135120, 121eqtr2d 2686 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝐹𝑓) = (𝐹𝑐))
136135csbeq1d 3573 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝐹𝑓) / 𝑧𝑆 = (𝐹𝑐) / 𝑧𝑆)
137136breqd 4696 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝑐(𝐹𝑓) / 𝑧𝑆𝑒𝑐(𝐹𝑐) / 𝑧𝑆𝑒))
138134, 137mtbid 313 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → ¬ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒)
139138expr 642 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ((𝐹𝑐) = (𝐹𝑒) → ¬ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒))
140 imnan 437 . . . . . . . . . . . . . . 15 (((𝐹𝑐) = (𝐹𝑒) → ¬ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒) ↔ ¬ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒))
141139, 140sylib 208 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ¬ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒))
142 ioran 510 . . . . . . . . . . . . . 14 (¬ ((𝐹𝑐)𝑅(𝐹𝑒) ∨ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒)) ↔ (¬ (𝐹𝑐)𝑅(𝐹𝑒) ∧ ¬ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒)))
143116, 141, 142sylanbrc 699 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ¬ ((𝐹𝑐)𝑅(𝐹𝑒) ∨ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒)))
14466, 67fnwe2val 37936 . . . . . . . . . . . . 13 (𝑐𝑇𝑒 ↔ ((𝐹𝑐)𝑅(𝐹𝑒) ∨ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒)))
145143, 144sylnibr 318 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ¬ 𝑐𝑇𝑒)
146145ralrimiva 2995 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) → ∀𝑐𝑎 ¬ 𝑐𝑇𝑒)
147 breq2 4689 . . . . . . . . . . . . . 14 (𝑏 = 𝑒 → (𝑐𝑇𝑏𝑐𝑇𝑒))
148147notbid 307 . . . . . . . . . . . . 13 (𝑏 = 𝑒 → (¬ 𝑐𝑇𝑏 ↔ ¬ 𝑐𝑇𝑒))
149148ralbidv 3015 . . . . . . . . . . . 12 (𝑏 = 𝑒 → (∀𝑐𝑎 ¬ 𝑐𝑇𝑏 ↔ ∀𝑐𝑎 ¬ 𝑐𝑇𝑒))
150149rspcev 3340 . . . . . . . . . . 11 ((𝑒𝑎 ∧ ∀𝑐𝑎 ¬ 𝑐𝑇𝑒) → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)
151104, 146, 150syl2anc 694 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)
152151ex 449 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) → (∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒) → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏))
153103, 152syl5bi 232 . . . . . . . 8 (((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) → (∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏))
154153ex 449 . . . . . . 7 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → ((𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓))) → (∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)))
15593, 154syl5bi 232 . . . . . 6 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) → (∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)))
156155rexlimdv 3059 . . . . 5 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (∃𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏))
15787, 156mpd 15 . . . 4 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)
158157rexlimdvaa 3061 . . 3 (𝜑 → (∃𝑓𝑎𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓) → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏))
15962, 158sylbid 230 . 2 (𝜑 → (∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏))
16027, 159mpd 15 1 (𝜑 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  {crab 2945  Vcvv 3231  csb 3566  cin 3606  wss 3607  c0 3948   class class class wbr 4685  {copab 4745   Fr wfr 5099   We wwe 5101  dom cdm 5143  ran crn 5144  cres 5145  cima 5146  Fun wfun 5920   Fn wfn 5921  wf 5922  cfv 5926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fv 5934
This theorem is referenced by:  fnwe2  37940
  Copyright terms: Public domain W3C validator