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 39161
Description: Lemma for fnwe2 39163. 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 6390 . . . 4 ((𝐹𝐴):𝐴𝐵 → Fun (𝐹𝐴))
3 vex 3440 . . . . 5 𝑎 ∈ V
43funimaex 6316 . . . 4 (Fun (𝐹𝐴) → ((𝐹𝐴) “ 𝑎) ∈ V)
51, 2, 43syl 18 . . 3 (𝜑 → ((𝐹𝐴) “ 𝑎) ∈ V)
6 fnwe2.r . . . 4 (𝜑𝑅 We 𝐵)
7 wefr 5438 . . . 4 (𝑅 We 𝐵𝑅 Fr 𝐵)
86, 7syl 17 . . 3 (𝜑𝑅 Fr 𝐵)
9 imassrn 5822 . . . 4 ((𝐹𝐴) “ 𝑎) ⊆ ran (𝐹𝐴)
101frnd 6394 . . . 4 (𝜑 → ran (𝐹𝐴) ⊆ 𝐵)
119, 10sstrid 3904 . . 3 (𝜑 → ((𝐹𝐴) “ 𝑎) ⊆ 𝐵)
12 incom 4103 . . . . . 6 (dom (𝐹𝐴) ∩ 𝑎) = (𝑎 ∩ dom (𝐹𝐴))
13 fnwe2lem2.a . . . . . . . 8 (𝜑𝑎𝐴)
141fdmd 6396 . . . . . . . 8 (𝜑 → dom (𝐹𝐴) = 𝐴)
1513, 14sseqtr4d 3933 . . . . . . 7 (𝜑𝑎 ⊆ dom (𝐹𝐴))
16 df-ss 3878 . . . . . . 7 (𝑎 ⊆ dom (𝐹𝐴) ↔ (𝑎 ∩ dom (𝐹𝐴)) = 𝑎)
1715, 16sylib 219 . . . . . 6 (𝜑 → (𝑎 ∩ dom (𝐹𝐴)) = 𝑎)
1812, 17syl5eq 2843 . . . . 5 (𝜑 → (dom (𝐹𝐴) ∩ 𝑎) = 𝑎)
19 fnwe2lem2.n0 . . . . 5 (𝜑𝑎 ≠ ∅)
2018, 19eqnetrd 3051 . . . 4 (𝜑 → (dom (𝐹𝐴) ∩ 𝑎) ≠ ∅)
21 imadisj 5829 . . . . 5 (((𝐹𝐴) “ 𝑎) = ∅ ↔ (dom (𝐹𝐴) ∩ 𝑎) = ∅)
2221necon3bii 3036 . . . 4 (((𝐹𝐴) “ 𝑎) ≠ ∅ ↔ (dom (𝐹𝐴) ∩ 𝑎) ≠ ∅)
2320, 22sylibr 235 . . 3 (𝜑 → ((𝐹𝐴) “ 𝑎) ≠ ∅)
24 fri 5410 . . 3 (((((𝐹𝐴) “ 𝑎) ∈ V ∧ 𝑅 Fr 𝐵) ∧ (((𝐹𝐴) “ 𝑎) ⊆ 𝐵 ∧ ((𝐹𝐴) “ 𝑎) ≠ ∅)) → ∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
255, 8, 11, 23, 24syl22anc 835 . 2 (𝜑 → ∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
26 df-ima 5461 . . . . . 6 ((𝐹𝐴) “ 𝑎) = ran ((𝐹𝐴) ↾ 𝑎)
2726rexeqi 3374 . . . . 5 (∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑑 ∈ ran ((𝐹𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑)
281ffnd 6388 . . . . . . 7 (𝜑 → (𝐹𝐴) Fn 𝐴)
29 fnssres 6345 . . . . . . 7 (((𝐹𝐴) Fn 𝐴𝑎𝐴) → ((𝐹𝐴) ↾ 𝑎) Fn 𝑎)
3028, 13, 29syl2anc 584 . . . . . 6 (𝜑 → ((𝐹𝐴) ↾ 𝑎) Fn 𝑎)
31 breq2 4970 . . . . . . . . 9 (𝑑 = (((𝐹𝐴) ↾ 𝑎)‘𝑓) → (𝑒𝑅𝑑𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3231notbid 319 . . . . . . . 8 (𝑑 = (((𝐹𝐴) ↾ 𝑎)‘𝑓) → (¬ 𝑒𝑅𝑑 ↔ ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3332ralbidv 3164 . . . . . . 7 (𝑑 = (((𝐹𝐴) ↾ 𝑎)‘𝑓) → (∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3433rexrn 6723 . . . . . 6 (((𝐹𝐴) ↾ 𝑎) Fn 𝑎 → (∃𝑑 ∈ ran ((𝐹𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓𝑎𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3530, 34syl 17 . . . . 5 (𝜑 → (∃𝑑 ∈ ran ((𝐹𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓𝑎𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3627, 35syl5bb 284 . . . 4 (𝜑 → (∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓𝑎𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3726raleqi 3373 . . . . . . . 8 (∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑒 ∈ ran ((𝐹𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓))
38 breq1 4969 . . . . . . . . . . 11 (𝑒 = (((𝐹𝐴) ↾ 𝑎)‘𝑑) → (𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
3938notbid 319 . . . . . . . . . 10 (𝑒 = (((𝐹𝐴) ↾ 𝑎)‘𝑑) → (¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4039ralrn 6724 . . . . . . . . 9 (((𝐹𝐴) ↾ 𝑎) Fn 𝑎 → (∀𝑒 ∈ ran ((𝐹𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4130, 40syl 17 . . . . . . . 8 (𝜑 → (∀𝑒 ∈ ran ((𝐹𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4237, 41syl5bb 284 . . . . . . 7 (𝜑 → (∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4342adantr 481 . . . . . 6 ((𝜑𝑓𝑎) → (∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓)))
4413resabs1d 5770 . . . . . . . . . . . 12 (𝜑 → ((𝐹𝐴) ↾ 𝑎) = (𝐹𝑎))
4544ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → ((𝐹𝐴) ↾ 𝑎) = (𝐹𝑎))
4645fveq1d 6545 . . . . . . . . . 10 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → (((𝐹𝐴) ↾ 𝑎)‘𝑑) = ((𝐹𝑎)‘𝑑))
47 fvres 6562 . . . . . . . . . . 11 (𝑑𝑎 → ((𝐹𝑎)‘𝑑) = (𝐹𝑑))
4847adantl 482 . . . . . . . . . 10 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → ((𝐹𝑎)‘𝑑) = (𝐹𝑑))
4946, 48eqtrd 2831 . . . . . . . . 9 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → (((𝐹𝐴) ↾ 𝑎)‘𝑑) = (𝐹𝑑))
5045fveq1d 6545 . . . . . . . . . 10 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → (((𝐹𝐴) ↾ 𝑎)‘𝑓) = ((𝐹𝑎)‘𝑓))
51 fvres 6562 . . . . . . . . . . 11 (𝑓𝑎 → ((𝐹𝑎)‘𝑓) = (𝐹𝑓))
5251ad2antlr 723 . . . . . . . . . 10 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → ((𝐹𝑎)‘𝑓) = (𝐹𝑓))
5350, 52eqtrd 2831 . . . . . . . . 9 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → (((𝐹𝐴) ↾ 𝑎)‘𝑓) = (𝐹𝑓))
5449, 53breq12d 4979 . . . . . . . 8 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → ((((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ (𝐹𝑑)𝑅(𝐹𝑓)))
5554notbid 319 . . . . . . 7 (((𝜑𝑓𝑎) ∧ 𝑑𝑎) → (¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ¬ (𝐹𝑑)𝑅(𝐹𝑓)))
5655ralbidva 3163 . . . . . 6 ((𝜑𝑓𝑎) → (∀𝑑𝑎 ¬ (((𝐹𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓)))
5743, 56bitrd 280 . . . . 5 ((𝜑𝑓𝑎) → (∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓)))
5857rexbidva 3259 . . . 4 (𝜑 → (∃𝑓𝑎𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹𝐴) ↾ 𝑎)‘𝑓) ↔ ∃𝑓𝑎𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓)))
5936, 58bitrd 280 . . 3 (𝜑 → (∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓𝑎𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓)))
603inex1 5117 . . . . . . 7 (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ∈ V
6160a1i 11 . . . . . 6 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ∈ V)
6213sselda 3893 . . . . . . . 8 ((𝜑𝑓𝑎) → 𝑓𝐴)
63 fnwe2.su . . . . . . . . . 10 (𝑧 = (𝐹𝑥) → 𝑆 = 𝑈)
64 fnwe2.t . . . . . . . . . 10 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝐹𝑥)𝑅(𝐹𝑦) ∨ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥𝑈𝑦))}
65 fnwe2.s . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝑈 We {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑥)})
6663, 64, 65fnwe2lem1 39160 . . . . . . . . 9 ((𝜑𝑓𝐴) → (𝐹𝑓) / 𝑧𝑆 We {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
67 wefr 5438 . . . . . . . . 9 ((𝐹𝑓) / 𝑧𝑆 We {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)} → (𝐹𝑓) / 𝑧𝑆 Fr {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
6866, 67syl 17 . . . . . . . 8 ((𝜑𝑓𝐴) → (𝐹𝑓) / 𝑧𝑆 Fr {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
6962, 68syldan 591 . . . . . . 7 ((𝜑𝑓𝑎) → (𝐹𝑓) / 𝑧𝑆 Fr {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
7069adantrr 713 . . . . . 6 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝐹𝑓) / 𝑧𝑆 Fr {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
71 inss2 4130 . . . . . . 7 (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ⊆ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}
7271a1i 11 . . . . . 6 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ⊆ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
73 simprl 767 . . . . . . . 8 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → 𝑓𝑎)
74 fveqeq2 6552 . . . . . . . . 9 (𝑦 = 𝑓 → ((𝐹𝑦) = (𝐹𝑓) ↔ (𝐹𝑓) = (𝐹𝑓)))
7562adantrr 713 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → 𝑓𝐴)
76 eqidd 2796 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝐹𝑓) = (𝐹𝑓))
7774, 75, 76elrabd 3621 . . . . . . . 8 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → 𝑓 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})
7873, 77elind 4096 . . . . . . 7 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → 𝑓 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}))
7978ne0d 4225 . . . . . 6 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ≠ ∅)
80 fri 5410 . . . . . 6 ((((𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ∈ V ∧ (𝐹𝑓) / 𝑧𝑆 Fr {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ∧ ((𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ⊆ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)} ∧ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ≠ ∅)) → ∃𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)
8161, 70, 72, 79, 80syl22anc 835 . . . . 5 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → ∃𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)
82 elin 4094 . . . . . . . 8 (𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑒𝑎𝑒 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}))
83 fveqeq2 6552 . . . . . . . . . 10 (𝑦 = 𝑒 → ((𝐹𝑦) = (𝐹𝑓) ↔ (𝐹𝑒) = (𝐹𝑓)))
8483elrab 3619 . . . . . . . . 9 (𝑒 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)} ↔ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))
8584anbi2i 622 . . . . . . . 8 ((𝑒𝑎𝑒 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓))))
8682, 85bitri 276 . . . . . . 7 (𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓))))
87 elin 4094 . . . . . . . . . . . . 13 (𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑔𝑎𝑔 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}))
88 fveqeq2 6552 . . . . . . . . . . . . . . 15 (𝑦 = 𝑔 → ((𝐹𝑦) = (𝐹𝑓) ↔ (𝐹𝑔) = (𝐹𝑓)))
8988elrab 3619 . . . . . . . . . . . . . 14 (𝑔 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)} ↔ (𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)))
9089anbi2i 622 . . . . . . . . . . . . 13 ((𝑔𝑎𝑔 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑔𝑎 ∧ (𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓))))
9187, 90bitri 276 . . . . . . . . . . . 12 (𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ↔ (𝑔𝑎 ∧ (𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓))))
9291imbi1i 351 . . . . . . . . . . 11 ((𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒) ↔ ((𝑔𝑎 ∧ (𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓))) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒))
93 impexp 451 . . . . . . . . . . 11 (((𝑔𝑎 ∧ (𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓))) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒) ↔ (𝑔𝑎 → ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)))
9492, 93bitri 276 . . . . . . . . . 10 ((𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒) ↔ (𝑔𝑎 → ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)))
9594ralbii2 3130 . . . . . . . . 9 (∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 ↔ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒))
96 simplrl 773 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) → 𝑒𝑎)
97 fveq2 6543 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑐 → (𝐹𝑑) = (𝐹𝑐))
9897breq1d 4976 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑐 → ((𝐹𝑑)𝑅(𝐹𝑓) ↔ (𝐹𝑐)𝑅(𝐹𝑓)))
9998notbid 319 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑐 → (¬ (𝐹𝑑)𝑅(𝐹𝑓) ↔ ¬ (𝐹𝑐)𝑅(𝐹𝑓)))
100 simplrr 774 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) → ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))
101100ad2antrr 722 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))
102 simpr 485 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → 𝑐𝑎)
10399, 101, 102rspcdva 3565 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ¬ (𝐹𝑐)𝑅(𝐹𝑓))
104 simprrr 778 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) → (𝐹𝑒) = (𝐹𝑓))
105104ad2antrr 722 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → (𝐹𝑒) = (𝐹𝑓))
106105breq2d 4978 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ((𝐹𝑐)𝑅(𝐹𝑒) ↔ (𝐹𝑐)𝑅(𝐹𝑓)))
107103, 106mtbird 326 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ¬ (𝐹𝑐)𝑅(𝐹𝑒))
10813ad3antrrr 726 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) → 𝑎𝐴)
109108sselda 3893 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → 𝑐𝐴)
110109adantrr 713 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → 𝑐𝐴)
111 simprr 769 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝐹𝑐) = (𝐹𝑒))
112104ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝐹𝑒) = (𝐹𝑓))
113111, 112eqtrd 2831 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝐹𝑐) = (𝐹𝑓))
114 eleq1w 2865 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑐 → (𝑔𝐴𝑐𝐴))
115 fveqeq2 6552 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑐 → ((𝐹𝑔) = (𝐹𝑓) ↔ (𝐹𝑐) = (𝐹𝑓)))
116114, 115anbi12d 630 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑐 → ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) ↔ (𝑐𝐴 ∧ (𝐹𝑐) = (𝐹𝑓))))
117 breq1 4969 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑐 → (𝑔(𝐹𝑓) / 𝑧𝑆𝑒𝑐(𝐹𝑓) / 𝑧𝑆𝑒))
118117notbid 319 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑐 → (¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 ↔ ¬ 𝑐(𝐹𝑓) / 𝑧𝑆𝑒))
119116, 118imbi12d 346 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑐 → (((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒) ↔ ((𝑐𝐴 ∧ (𝐹𝑐) = (𝐹𝑓)) → ¬ 𝑐(𝐹𝑓) / 𝑧𝑆𝑒)))
120 simplr 765 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒))
121 simprl 767 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → 𝑐𝑎)
122119, 120, 121rspcdva 3565 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → ((𝑐𝐴 ∧ (𝐹𝑐) = (𝐹𝑓)) → ¬ 𝑐(𝐹𝑓) / 𝑧𝑆𝑒))
123110, 113, 122mp2and 695 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → ¬ 𝑐(𝐹𝑓) / 𝑧𝑆𝑒)
124111, 112eqtr2d 2832 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝐹𝑓) = (𝐹𝑐))
125124csbeq1d 3819 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝐹𝑓) / 𝑧𝑆 = (𝐹𝑐) / 𝑧𝑆)
126125breqd 4977 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → (𝑐(𝐹𝑓) / 𝑧𝑆𝑒𝑐(𝐹𝑐) / 𝑧𝑆𝑒))
127123, 126mtbid 325 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ (𝑐𝑎 ∧ (𝐹𝑐) = (𝐹𝑒))) → ¬ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒)
128127expr 457 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ((𝐹𝑐) = (𝐹𝑒) → ¬ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒))
129 imnan 400 . . . . . . . . . . . . . . 15 (((𝐹𝑐) = (𝐹𝑒) → ¬ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒) ↔ ¬ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒))
130128, 129sylib 219 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ¬ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒))
131 ioran 978 . . . . . . . . . . . . . 14 (¬ ((𝐹𝑐)𝑅(𝐹𝑒) ∨ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒)) ↔ (¬ (𝐹𝑐)𝑅(𝐹𝑒) ∧ ¬ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒)))
132107, 130, 131sylanbrc 583 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ¬ ((𝐹𝑐)𝑅(𝐹𝑒) ∨ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒)))
13363, 64fnwe2val 39159 . . . . . . . . . . . . 13 (𝑐𝑇𝑒 ↔ ((𝐹𝑐)𝑅(𝐹𝑒) ∨ ((𝐹𝑐) = (𝐹𝑒) ∧ 𝑐(𝐹𝑐) / 𝑧𝑆𝑒)))
134132, 133sylnibr 330 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) ∧ 𝑐𝑎) → ¬ 𝑐𝑇𝑒)
135134ralrimiva 3149 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) → ∀𝑐𝑎 ¬ 𝑐𝑇𝑒)
136 breq2 4970 . . . . . . . . . . . . . 14 (𝑏 = 𝑒 → (𝑐𝑇𝑏𝑐𝑇𝑒))
137136notbid 319 . . . . . . . . . . . . 13 (𝑏 = 𝑒 → (¬ 𝑐𝑇𝑏 ↔ ¬ 𝑐𝑇𝑒))
138137ralbidv 3164 . . . . . . . . . . . 12 (𝑏 = 𝑒 → (∀𝑐𝑎 ¬ 𝑐𝑇𝑏 ↔ ∀𝑐𝑎 ¬ 𝑐𝑇𝑒))
139138rspcev 3559 . . . . . . . . . . 11 ((𝑒𝑎 ∧ ∀𝑐𝑎 ¬ 𝑐𝑇𝑒) → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)
14096, 135, 139syl2anc 584 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) ∧ ∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒)) → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)
141140ex 413 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) → (∀𝑔𝑎 ((𝑔𝐴 ∧ (𝐹𝑔) = (𝐹𝑓)) → ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒) → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏))
14295, 141syl5bi 243 . . . . . . . 8 (((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) ∧ (𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓)))) → (∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏))
143142ex 413 . . . . . . 7 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → ((𝑒𝑎 ∧ (𝑒𝐴 ∧ (𝐹𝑒) = (𝐹𝑓))) → (∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)))
14486, 143syl5bi 243 . . . . . 6 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) → (∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)))
145144rexlimdv 3246 . . . . 5 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → (∃𝑒 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑓)}) ¬ 𝑔(𝐹𝑓) / 𝑧𝑆𝑒 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏))
14681, 145mpd 15 . . . 4 ((𝜑 ∧ (𝑓𝑎 ∧ ∀𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓))) → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)
147146rexlimdvaa 3248 . . 3 (𝜑 → (∃𝑓𝑎𝑑𝑎 ¬ (𝐹𝑑)𝑅(𝐹𝑓) → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏))
14859, 147sylbid 241 . 2 (𝜑 → (∃𝑑 ∈ ((𝐹𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏))
14925, 148mpd 15 1 (𝜑 → ∃𝑏𝑎𝑐𝑎 ¬ 𝑐𝑇𝑏)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 842   = wceq 1522  wcel 2081  wne 2984  wral 3105  wrex 3106  {crab 3109  Vcvv 3437  csb 3815  cin 3862  wss 3863  c0 4215   class class class wbr 4966  {copab 5028   Fr wfr 5404   We wwe 5406  dom cdm 5448  ran crn 5449  cres 5450  cima 5451  Fun wfun 6224   Fn wfn 6225  wf 6226  cfv 6230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5086  ax-sep 5099  ax-nul 5106  ax-pr 5226
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3710  df-csb 3816  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-br 4967  df-opab 5029  df-mpt 5046  df-id 5353  df-po 5367  df-so 5368  df-fr 5407  df-we 5409  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-res 5460  df-ima 5461  df-iota 6194  df-fun 6232  df-fn 6233  df-f 6234  df-fv 6238
This theorem is referenced by:  fnwe2  39163
  Copyright terms: Public domain W3C validator