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 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.
StepHypRef Expression
1 fnwe2.f . . . 4 (𝜑 → (𝐹𝐴):𝐴𝐵)
2 ffun 6226 . . . 4 ((𝐹𝐴):𝐴𝐵 → Fun (𝐹𝐴))
3 vex 3353 . . . . 5 𝑎 ∈ V
43funimaex 6154 . . . 4 (Fun (𝐹𝐴) → ((𝐹𝐴) “ 𝑎) ∈ V)
51, 2, 43syl 18 . . 3 (𝜑 → ((𝐹𝐴) “ 𝑎) ∈ V)
6 fnwe2.r . . . 4 (𝜑𝑅 We 𝐵)
7 wefr 5267 . . . 4 (𝑅 We 𝐵𝑅 Fr 𝐵)
86, 7syl 17 . . 3 (𝜑𝑅 Fr 𝐵)
9 imassrn 5659 . . . 4 ((𝐹𝐴) “ 𝑎) ⊆ ran (𝐹𝐴)
101frnd 6230 . . . 4 (𝜑 → ran (𝐹𝐴) ⊆ 𝐵)
119, 10syl5ss 3772 . . 3 (𝜑 → ((𝐹𝐴) “ 𝑎) ⊆ 𝐵)
12 incom 3967 . . . . . 6 (dom (𝐹𝐴) ∩ 𝑎) = (𝑎 ∩ dom (𝐹𝐴))
13 fnwe2lem2.a . . . . . . . 8 (𝜑𝑎𝐴)
141fdmd 6232 . . . . . . . 8 (𝜑 → dom (𝐹𝐴) = 𝐴)
1513, 14sseqtr4d 3802 . . . . . . 7 (𝜑𝑎 ⊆ dom (𝐹𝐴))
16 df-ss 3746 . . . . . . 7 (𝑎 ⊆ dom (𝐹𝐴) ↔ (𝑎 ∩ dom (𝐹𝐴)) = 𝑎)
1715, 16sylib 209 . . . . . 6 (𝜑 → (𝑎 ∩ dom (𝐹𝐴)) = 𝑎)
1812, 17syl5eq 2811 . . . . 5 (𝜑 → (dom (𝐹𝐴) ∩ 𝑎) = 𝑎)
19 fnwe2lem2.n0 . . . . 5 (𝜑𝑎 ≠ ∅)
2018, 19eqnetrd 3004 . . . 4 (𝜑 → (dom (𝐹𝐴) ∩ 𝑎) ≠ ∅)
21 imadisj 5666 . . . . 5 (((𝐹𝐴) “ 𝑎) = ∅ ↔ (dom (𝐹𝐴) ∩ 𝑎) = ∅)
2221necon3bii 2989 . . . 4 (((𝐹𝐴) “ 𝑎) ≠ ∅ ↔ (dom (𝐹𝐴) ∩ 𝑎) ≠ ∅)
2320, 22sylibr 225 . . 3 (𝜑 → ((𝐹𝐴) “ 𝑎) ≠ ∅)
24 fri 5239 . . 3 (((((𝐹𝐴) “ 𝑎) ∈ V ∧ 𝑅 Fr 𝐵) ∧ (((𝐹𝐴) “ 𝑎) ⊆ 𝐵 ∧ ((𝐹𝐴) “ 𝑎) ≠ ∅)) → ∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
255, 8, 11, 23, 24syl22anc 867 . 2 (𝜑 → ∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
26 df-ima 5290 . . . . . 6 ((𝐹𝐴) “ 𝑎) = ran ((𝐹𝐴) ↾ 𝑎)
2726rexeqi 3291 . . . . 5 (∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑑 ∈ ran ((𝐹𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
281ffnd 6224 . . . . . . 7 (𝜑 → (𝐹𝐴) Fn 𝐴)
29 fnssres 6182 . . . . . . 7 (((𝐹𝐴) Fn 𝐴𝑎𝐴) → ((𝐹𝐴) ↾ 𝑎) Fn 𝑎)
3028, 13, 29syl2anc 579 . . . . . 6 (𝜑 → ((𝐹𝐴) ↾ 𝑎) Fn 𝑎)
31 breq2 4813 . . . . . . . . 9 (𝑑 = (((𝐹𝐴) ↾ 𝑎)‘𝑓) → (𝑒𝑅𝑑𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3231notbid 309 . . . . . . . 8 (𝑑 = (((𝐹𝐴) ↾ 𝑎)‘𝑓) → (¬ 𝑒𝑅𝑑 ↔ ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3332ralbidv 3133 . . . . . . 7 (𝑑 = (((𝐹𝐴) ↾ 𝑎)‘𝑓) → (∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3433rexrn 6551 . . . . . 6 (((𝐹𝐴) ↾ 𝑎) Fn 𝑎 → (∃𝑑 ∈ ran ((𝐹𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓𝑎𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3530, 34syl 17 . . . . 5 (𝜑 → (∃𝑑 ∈ ran ((𝐹𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓𝑎𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3627, 35syl5bb 274 . . . 4 (𝜑 → (∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓𝑎𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3726raleqi 3290 . . . . . . . 8 (∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑒 ∈ ran ((𝐹𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓))
38 breq1 4812 . . . . . . . . . . 11 (𝑒 = (((𝐹𝐴) ↾ 𝑎)‘𝑑) → (𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3938notbid 309 . . . . . . . . . 10 (𝑒 = (((𝐹𝐴) ↾ 𝑎)‘𝑑) → (¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4039ralrn 6552 . . . . . . . . 9 (((𝐹𝐴) ↾ 𝑎) Fn 𝑎 → (∀𝑒 ∈ ran ((𝐹𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4130, 40syl 17 . . . . . . . 8 (𝜑 → (∀𝑒 ∈ ran ((𝐹𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4237, 41syl5bb 274 . . . . . . 7 (𝜑 → (∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4342adantr 472 . . . . . 6 ((𝜑𝑓𝑎) → (∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4413resabs1d 5603 . . . . . . . . . . . 12 (𝜑 → ((𝐹𝐴) ↾ 𝑎) = (𝐹𝑎))
4544ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → ((𝐹𝐴) ↾ 𝑎) = (𝐹𝑎))
4645fveq1d 6377 . . . . . . . . . 10 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → (((𝐹𝐴) ↾ 𝑎)‘𝑑) = ((𝐹𝑎)‘𝑑))
47 fvres 6394 . . . . . . . . . . 11 (𝑑𝑎 → ((𝐹𝑎)‘𝑑) = (𝐹𝑑))
4847adantl 473 . . . . . . . . . 10 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → ((𝐹𝑎)‘𝑑) = (𝐹𝑑))
4946, 48eqtrd 2799 . . . . . . . . 9 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → (((𝐹𝐴) ↾ 𝑎)‘𝑑) = (𝐹𝑑))
5045fveq1d 6377 . . . . . . . . . 10 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → (((𝐹𝐴) ↾ 𝑎)‘𝑓) = ((𝐹𝑎)‘𝑓))
51 fvres 6394 . . . . . . . . . . 11 (𝑓𝑎 → ((𝐹𝑎)‘𝑓) = (𝐹𝑓))
5251ad2antlr 718 . . . . . . . . . 10 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → ((𝐹𝑎)‘𝑓) = (𝐹𝑓))
5350, 52eqtrd 2799 . . . . . . . . 9 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → (((𝐹𝐴) ↾ 𝑎)‘𝑓) = (𝐹𝑓))
5449, 53breq12d 4822 . . . . . . . 8 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → ((((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ (𝐹𝑑)𝑅(𝐹𝑓)))
5554notbid 309 . . . . . . 7 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → (¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ¬ (𝐹𝑑)𝑅(𝐹𝑓)))
5655ralbidva 3132 . . . . . 6 ((𝜑𝑓𝑎) → (∀𝑑𝑎 ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓)))
5743, 56bitrd 270 . . . . 5 ((𝜑𝑓𝑎) → (∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓)))
5857rexbidva 3196 . . . 4 (𝜑 → (∃𝑓𝑎𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∃𝑓𝑎𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓)))
5936, 58bitrd 270 . . 3 (𝜑 → (∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓𝑎𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓)))
603inex1 4960 . . . . . . 7 (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ∈ V
6160a1i 11 . . . . . 6 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ∈ V)
6213sselda 3761 . . . . . . . 8 ((𝜑𝑓𝑎) → 𝑓𝐴)
63 fnwe2.su . . . . . . . . . 10 (𝑧 = (𝐹𝑥) → 𝑆 = 𝑈)
64 fnwe2.t . . . . . . . . . 10 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝐹𝑥)𝑅(𝐹𝑦) ∨ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥𝑈𝑦))}
65 fnwe2.s . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝑈 We {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑥)})
6663, 64, 65fnwe2lem1 38229 . . . . . . . . 9 ((𝜑𝑓𝐴) → (𝐹𝑓) / 𝑧𝑆 We {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
67 wefr 5267 . . . . . . . . 9 ((𝐹𝑓) / 𝑧𝑆 We {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)} → (𝐹𝑓) / 𝑧𝑆 Fr {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
6866, 67syl 17 . . . . . . . 8 ((𝜑𝑓𝐴) → (𝐹𝑓) / 𝑧𝑆 Fr {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
6962, 68syldan 585 . . . . . . 7 ((𝜑𝑓𝑎) → (𝐹𝑓) / 𝑧𝑆 Fr {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
7069adantrr 708 . . . . . 6 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝐹𝑓) / 𝑧𝑆 Fr {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
71 inss2 3993 . . . . . . 7 (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ⊆ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}
7271a1i 11 . . . . . 6 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ⊆ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
73 simprl 787 . . . . . . . 8 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → 𝑓𝑎)
7462adantrr 708 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → 𝑓𝐴)
75 eqidd 2766 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝐹𝑓) = (𝐹𝑓))
76 fveqeq2 6384 . . . . . . . . . 10 (𝑦 = 𝑓 → ((𝐹𝑦) = (𝐹𝑓) ↔ (𝐹𝑓) = (𝐹𝑓)))
7776elrab 3519 . . . . . . . . 9 (𝑓 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)} ↔ (𝑓𝐴 ∧ (𝐹𝑓) = (𝐹𝑓)))
7874, 75, 77sylanbrc 578 . . . . . . . 8 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → 𝑓 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
7973, 78elind 3960 . . . . . . 7 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → 𝑓 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}))
8079ne0d 4086 . . . . . 6 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ≠ ∅)
81 fri 5239 . . . . . 6 ((((𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ∈ V ∧ (𝐹𝑓) / 𝑧𝑆 Fr {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ∧ ((𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ⊆ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)} ∧ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ≠ ∅)) → ∃𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)
8261, 70, 72, 80, 81syl22anc 867 . . . . 5 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → ∃𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)
83 elin 3958 . . . . . . . 8 (𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑒𝑎𝑒 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}))
84 fveqeq2 6384 . . . . . . . . . 10 (𝑦 = 𝑒 → ((𝐹𝑦) = (𝐹𝑓) ↔ (𝐹𝑒) = (𝐹𝑓)))
8584elrab 3519 . . . . . . . . 9 (𝑒 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)} ↔ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))
8685anbi2i 616 . . . . . . . 8 ((𝑒𝑎𝑒 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓))))
8783, 86bitri 266 . . . . . . 7 (𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓))))
88 elin 3958 . . . . . . . . . . . . 13 (𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑔𝑎𝑔 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}))
89 fveqeq2 6384 . . . . . . . . . . . . . . 15 (𝑦 = 𝑔 → ((𝐹𝑦) = (𝐹𝑓) ↔ (𝐹𝑔) = (𝐹𝑓)))
9089elrab 3519 . . . . . . . . . . . . . 14 (𝑔 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)} ↔ (𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)))
9190anbi2i 616 . . . . . . . . . . . . 13 ((𝑔𝑎𝑔 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑔𝑎 ∧ (𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓))))
9288, 91bitri 266 . . . . . . . . . . . 12 (𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑔𝑎 ∧ (𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓))))
9392imbi1i 340 . . . . . . . . . . 11 ((𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒) ↔ ((𝑔𝑎 ∧ (𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓))) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒))
94 impexp 441 . . . . . . . . . . 11 (((𝑔𝑎 ∧ (𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓))) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒) ↔ (𝑔𝑎 → ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)))
9593, 94bitri 266 . . . . . . . . . 10 ((𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒) ↔ (𝑔𝑎 → ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)))
9695ralbii2 3125 . . . . . . . . 9 (∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 ↔ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒))
97 simplrl 795 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) → 𝑒𝑎)
98 simpr 477 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → 𝑐𝑎)
99 simplrr 796 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) → ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))
10099ad2antrr 717 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))
101 fveq2 6375 . . . . . . . . . . . . . . . . . . 19 (𝑑 = 𝑐 → (𝐹𝑑) = (𝐹𝑐))
102101breq1d 4819 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑐 → ((𝐹𝑑)𝑅(𝐹𝑓) ↔ (𝐹𝑐)𝑅(𝐹𝑓)))
103102notbid 309 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑐 → (¬ (𝐹𝑑)𝑅(𝐹𝑓) ↔ ¬ (𝐹𝑐)𝑅(𝐹𝑓)))
104103rspcva 3459 . . . . . . . . . . . . . . . 16 ((𝑐𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓)) → ¬ (𝐹𝑐)𝑅(𝐹𝑓))
10598, 100, 104syl2anc 579 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ¬ (𝐹𝑐)𝑅(𝐹𝑓))
106 simprrr 800 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) → (𝐹𝑒) = (𝐹𝑓))
107106ad2antrr 717 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → (𝐹𝑒) = (𝐹𝑓))
108107breq2d 4821 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ((𝐹𝑐)𝑅(𝐹𝑒) ↔ (𝐹𝑐)𝑅(𝐹𝑓)))
109105, 108mtbird 316 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ¬ (𝐹𝑐)𝑅(𝐹𝑒))
11013ad3antrrr 721 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) → 𝑎𝐴)
111110sselda 3761 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → 𝑐𝐴)
112111adantrr 708 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → 𝑐𝐴)
113 simprr 789 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝐹𝑐) = (𝐹𝑒))
114106ad2antrr 717 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝐹𝑒) = (𝐹𝑓))
115113, 114eqtrd 2799 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝐹𝑐) = (𝐹𝑓))
116 simprl 787 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → 𝑐𝑎)
117 simplr 785 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒))
118 eleq1w 2827 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝑐 → (𝑔𝐴𝑐𝐴))
119 fveqeq2 6384 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝑐 → ((𝐹𝑔) = (𝐹𝑓) ↔ (𝐹𝑐) = (𝐹𝑓)))
120118, 119anbi12d 624 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑐 → ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) ↔ (𝑐𝐴 ∧ (𝐹𝑐) = (𝐹𝑓))))
121 breq1 4812 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝑐 → (𝑔(𝐹𝑓) / 𝑧𝑆𝑒𝑐(𝐹𝑓) / 𝑧𝑆𝑒))
122121notbid 309 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑐 → (¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 ↔ ¬ 𝑐(𝐹𝑓) / 𝑧𝑆𝑒))
123120, 122imbi12d 335 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑐 → (((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒) ↔ ((𝑐𝐴 ∧ (𝐹𝑐) = (𝐹𝑓)) → ¬ 𝑐(𝐹𝑓) / 𝑧𝑆𝑒)))
124123rspcva 3459 . . . . . . . . . . . . . . . . . . 19 ((𝑐𝑎 ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) → ((𝑐𝐴 ∧ (𝐹𝑐) = (𝐹𝑓)) → ¬ 𝑐(𝐹𝑓) / 𝑧𝑆𝑒))
125116, 117, 124syl2anc 579 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → ((𝑐𝐴 ∧ (𝐹𝑐) = (𝐹𝑓)) → ¬ 𝑐(𝐹𝑓) / 𝑧𝑆𝑒))
126112, 115, 125mp2and 690 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → ¬ 𝑐(𝐹𝑓) / 𝑧𝑆𝑒)
127113, 114eqtr2d 2800 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝐹𝑓) = (𝐹𝑐))
128127csbeq1d 3698 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝐹𝑓) / 𝑧𝑆 = (𝐹𝑐) / 𝑧𝑆)
129128breqd 4820 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝑐(𝐹𝑓) / 𝑧𝑆𝑒𝑐(𝐹𝑐) / 𝑧𝑆𝑒))
130126, 129mtbid 315 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → ¬ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒)
131130expr 448 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ((𝐹𝑐) = (𝐹𝑒) → ¬ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒))
132 imnan 388 . . . . . . . . . . . . . . 15 (((𝐹𝑐) = (𝐹𝑒) → ¬ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒) ↔ ¬ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒))
133131, 132sylib 209 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ¬ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒))
134 ioran 1006 . . . . . . . . . . . . . 14 (¬ ((𝐹𝑐)𝑅(𝐹𝑒) ∨ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒)) ↔ (¬ (𝐹𝑐)𝑅(𝐹𝑒) ∧ ¬ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒)))
135109, 133, 134sylanbrc 578 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ¬ ((𝐹𝑐)𝑅(𝐹𝑒) ∨ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒)))
13663, 64fnwe2val 38228 . . . . . . . . . . . . 13 (𝑐𝑇𝑒 ↔ ((𝐹𝑐)𝑅(𝐹𝑒) ∨ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒)))
137135, 136sylnibr 320 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ¬ 𝑐𝑇𝑒)
138137ralrimiva 3113 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) → ∀𝑐𝑎 ¬ 𝑐𝑇𝑒)
139 breq2 4813 . . . . . . . . . . . . . 14 (𝑏 = 𝑒 → (𝑐𝑇𝑏𝑐𝑇𝑒))
140139notbid 309 . . . . . . . . . . . . 13 (𝑏 = 𝑒 → (¬ 𝑐𝑇𝑏 ↔ ¬ 𝑐𝑇𝑒))
141140ralbidv 3133 . . . . . . . . . . . 12 (𝑏 = 𝑒 → (∀𝑐𝑎 ¬ 𝑐𝑇𝑏 ↔ ∀𝑐𝑎 ¬ 𝑐𝑇𝑒))
142141rspcev 3461 . . . . . . . . . . 11 ((𝑒𝑎 ∧ ∀𝑐𝑎 ¬ 𝑐𝑇𝑒) → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)
14397, 138, 142syl2anc 579 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)
144143ex 401 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) → (∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒) → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏))
14596, 144syl5bi 233 . . . . . . . 8 (((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) → (∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏))
146145ex 401 . . . . . . 7 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → ((𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓))) → (∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)))
14787, 146syl5bi 233 . . . . . 6 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) → (∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)))
148147rexlimdv 3177 . . . . 5 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (∃𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏))
14982, 148mpd 15 . . . 4 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)
150149rexlimdvaa 3179 . . 3 (𝜑 → (∃𝑓𝑎𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓) → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏))
15159, 150sylbid 231 . 2 (𝜑 → (∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏))
15225, 151mpd 15 1 (𝜑 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator