Metamath Proof Explorer


Theorem fnwe2lem2

Description: Lemma for fnwe2 . An element which is in a minimal fiber and minimal within its fiber is minimal globally; thus T is well-founded. (Contributed by Stefan O'Rear, 19-Jan-2015)

Ref Expression
Hypotheses fnwe2.su ( 𝑧 = ( 𝐹𝑥 ) → 𝑆 = 𝑈 )
fnwe2.t 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝐹𝑥 ) 𝑅 ( 𝐹𝑦 ) ∨ ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) ∧ 𝑥 𝑈 𝑦 ) ) }
fnwe2.s ( ( 𝜑𝑥𝐴 ) → 𝑈 We { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑥 ) } )
fnwe2.f ( 𝜑 → ( 𝐹𝐴 ) : 𝐴𝐵 )
fnwe2.r ( 𝜑𝑅 We 𝐵 )
fnwe2lem2.a ( 𝜑𝑎𝐴 )
fnwe2lem2.n0 ( 𝜑𝑎 ≠ ∅ )
Assertion fnwe2lem2 ( 𝜑 → ∃ 𝑏𝑎𝑐𝑎 ¬ 𝑐 𝑇 𝑏 )

Proof

Step Hyp Ref Expression
1 fnwe2.su ( 𝑧 = ( 𝐹𝑥 ) → 𝑆 = 𝑈 )
2 fnwe2.t 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝐹𝑥 ) 𝑅 ( 𝐹𝑦 ) ∨ ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) ∧ 𝑥 𝑈 𝑦 ) ) }
3 fnwe2.s ( ( 𝜑𝑥𝐴 ) → 𝑈 We { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑥 ) } )
4 fnwe2.f ( 𝜑 → ( 𝐹𝐴 ) : 𝐴𝐵 )
5 fnwe2.r ( 𝜑𝑅 We 𝐵 )
6 fnwe2lem2.a ( 𝜑𝑎𝐴 )
7 fnwe2lem2.n0 ( 𝜑𝑎 ≠ ∅ )
8 ffun ( ( 𝐹𝐴 ) : 𝐴𝐵 → Fun ( 𝐹𝐴 ) )
9 vex 𝑎 ∈ V
10 9 funimaex ( Fun ( 𝐹𝐴 ) → ( ( 𝐹𝐴 ) “ 𝑎 ) ∈ V )
11 4 8 10 3syl ( 𝜑 → ( ( 𝐹𝐴 ) “ 𝑎 ) ∈ V )
12 wefr ( 𝑅 We 𝐵𝑅 Fr 𝐵 )
13 5 12 syl ( 𝜑𝑅 Fr 𝐵 )
14 imassrn ( ( 𝐹𝐴 ) “ 𝑎 ) ⊆ ran ( 𝐹𝐴 )
15 4 frnd ( 𝜑 → ran ( 𝐹𝐴 ) ⊆ 𝐵 )
16 14 15 sstrid ( 𝜑 → ( ( 𝐹𝐴 ) “ 𝑎 ) ⊆ 𝐵 )
17 incom ( dom ( 𝐹𝐴 ) ∩ 𝑎 ) = ( 𝑎 ∩ dom ( 𝐹𝐴 ) )
18 4 fdmd ( 𝜑 → dom ( 𝐹𝐴 ) = 𝐴 )
19 6 18 sseqtrrd ( 𝜑𝑎 ⊆ dom ( 𝐹𝐴 ) )
20 df-ss ( 𝑎 ⊆ dom ( 𝐹𝐴 ) ↔ ( 𝑎 ∩ dom ( 𝐹𝐴 ) ) = 𝑎 )
21 19 20 sylib ( 𝜑 → ( 𝑎 ∩ dom ( 𝐹𝐴 ) ) = 𝑎 )
22 17 21 syl5eq ( 𝜑 → ( dom ( 𝐹𝐴 ) ∩ 𝑎 ) = 𝑎 )
23 22 7 eqnetrd ( 𝜑 → ( dom ( 𝐹𝐴 ) ∩ 𝑎 ) ≠ ∅ )
24 imadisj ( ( ( 𝐹𝐴 ) “ 𝑎 ) = ∅ ↔ ( dom ( 𝐹𝐴 ) ∩ 𝑎 ) = ∅ )
25 24 necon3bii ( ( ( 𝐹𝐴 ) “ 𝑎 ) ≠ ∅ ↔ ( dom ( 𝐹𝐴 ) ∩ 𝑎 ) ≠ ∅ )
26 23 25 sylibr ( 𝜑 → ( ( 𝐹𝐴 ) “ 𝑎 ) ≠ ∅ )
27 fri ( ( ( ( ( 𝐹𝐴 ) “ 𝑎 ) ∈ V ∧ 𝑅 Fr 𝐵 ) ∧ ( ( ( 𝐹𝐴 ) “ 𝑎 ) ⊆ 𝐵 ∧ ( ( 𝐹𝐴 ) “ 𝑎 ) ≠ ∅ ) ) → ∃ 𝑑 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ∀ 𝑒 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 𝑑 )
28 11 13 16 26 27 syl22anc ( 𝜑 → ∃ 𝑑 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ∀ 𝑒 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 𝑑 )
29 df-ima ( ( 𝐹𝐴 ) “ 𝑎 ) = ran ( ( 𝐹𝐴 ) ↾ 𝑎 )
30 29 rexeqi ( ∃ 𝑑 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ∀ 𝑒 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 𝑑 ↔ ∃ 𝑑 ∈ ran ( ( 𝐹𝐴 ) ↾ 𝑎 ) ∀ 𝑒 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 𝑑 )
31 4 ffnd ( 𝜑 → ( 𝐹𝐴 ) Fn 𝐴 )
32 fnssres ( ( ( 𝐹𝐴 ) Fn 𝐴𝑎𝐴 ) → ( ( 𝐹𝐴 ) ↾ 𝑎 ) Fn 𝑎 )
33 31 6 32 syl2anc ( 𝜑 → ( ( 𝐹𝐴 ) ↾ 𝑎 ) Fn 𝑎 )
34 breq2 ( 𝑑 = ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) → ( 𝑒 𝑅 𝑑𝑒 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ) )
35 34 notbid ( 𝑑 = ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) → ( ¬ 𝑒 𝑅 𝑑 ↔ ¬ 𝑒 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ) )
36 35 ralbidv ( 𝑑 = ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) → ( ∀ 𝑒 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 𝑑 ↔ ∀ 𝑒 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ) )
37 36 rexrn ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) Fn 𝑎 → ( ∃ 𝑑 ∈ ran ( ( 𝐹𝐴 ) ↾ 𝑎 ) ∀ 𝑒 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 𝑑 ↔ ∃ 𝑓𝑎𝑒 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ) )
38 33 37 syl ( 𝜑 → ( ∃ 𝑑 ∈ ran ( ( 𝐹𝐴 ) ↾ 𝑎 ) ∀ 𝑒 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 𝑑 ↔ ∃ 𝑓𝑎𝑒 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ) )
39 30 38 syl5bb ( 𝜑 → ( ∃ 𝑑 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ∀ 𝑒 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 𝑑 ↔ ∃ 𝑓𝑎𝑒 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ) )
40 29 raleqi ( ∀ 𝑒 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ↔ ∀ 𝑒 ∈ ran ( ( 𝐹𝐴 ) ↾ 𝑎 ) ¬ 𝑒 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) )
41 breq1 ( 𝑒 = ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑑 ) → ( 𝑒 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ↔ ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑑 ) 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ) )
42 41 notbid ( 𝑒 = ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑑 ) → ( ¬ 𝑒 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ↔ ¬ ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑑 ) 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ) )
43 42 ralrn ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) Fn 𝑎 → ( ∀ 𝑒 ∈ ran ( ( 𝐹𝐴 ) ↾ 𝑎 ) ¬ 𝑒 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ↔ ∀ 𝑑𝑎 ¬ ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑑 ) 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ) )
44 33 43 syl ( 𝜑 → ( ∀ 𝑒 ∈ ran ( ( 𝐹𝐴 ) ↾ 𝑎 ) ¬ 𝑒 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ↔ ∀ 𝑑𝑎 ¬ ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑑 ) 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ) )
45 40 44 syl5bb ( 𝜑 → ( ∀ 𝑒 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ↔ ∀ 𝑑𝑎 ¬ ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑑 ) 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ) )
46 45 adantr ( ( 𝜑𝑓𝑎 ) → ( ∀ 𝑒 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ↔ ∀ 𝑑𝑎 ¬ ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑑 ) 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ) )
47 6 resabs1d ( 𝜑 → ( ( 𝐹𝐴 ) ↾ 𝑎 ) = ( 𝐹𝑎 ) )
48 47 ad2antrr ( ( ( 𝜑𝑓𝑎 ) ∧ 𝑑𝑎 ) → ( ( 𝐹𝐴 ) ↾ 𝑎 ) = ( 𝐹𝑎 ) )
49 48 fveq1d ( ( ( 𝜑𝑓𝑎 ) ∧ 𝑑𝑎 ) → ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑑 ) = ( ( 𝐹𝑎 ) ‘ 𝑑 ) )
50 fvres ( 𝑑𝑎 → ( ( 𝐹𝑎 ) ‘ 𝑑 ) = ( 𝐹𝑑 ) )
51 50 adantl ( ( ( 𝜑𝑓𝑎 ) ∧ 𝑑𝑎 ) → ( ( 𝐹𝑎 ) ‘ 𝑑 ) = ( 𝐹𝑑 ) )
52 49 51 eqtrd ( ( ( 𝜑𝑓𝑎 ) ∧ 𝑑𝑎 ) → ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑑 ) = ( 𝐹𝑑 ) )
53 48 fveq1d ( ( ( 𝜑𝑓𝑎 ) ∧ 𝑑𝑎 ) → ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) = ( ( 𝐹𝑎 ) ‘ 𝑓 ) )
54 fvres ( 𝑓𝑎 → ( ( 𝐹𝑎 ) ‘ 𝑓 ) = ( 𝐹𝑓 ) )
55 54 ad2antlr ( ( ( 𝜑𝑓𝑎 ) ∧ 𝑑𝑎 ) → ( ( 𝐹𝑎 ) ‘ 𝑓 ) = ( 𝐹𝑓 ) )
56 53 55 eqtrd ( ( ( 𝜑𝑓𝑎 ) ∧ 𝑑𝑎 ) → ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) = ( 𝐹𝑓 ) )
57 52 56 breq12d ( ( ( 𝜑𝑓𝑎 ) ∧ 𝑑𝑎 ) → ( ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑑 ) 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ↔ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) )
58 57 notbid ( ( ( 𝜑𝑓𝑎 ) ∧ 𝑑𝑎 ) → ( ¬ ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑑 ) 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ↔ ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) )
59 58 ralbidva ( ( 𝜑𝑓𝑎 ) → ( ∀ 𝑑𝑎 ¬ ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑑 ) 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ↔ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) )
60 46 59 bitrd ( ( 𝜑𝑓𝑎 ) → ( ∀ 𝑒 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ↔ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) )
61 60 rexbidva ( 𝜑 → ( ∃ 𝑓𝑎𝑒 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 ( ( ( 𝐹𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ↔ ∃ 𝑓𝑎𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) )
62 39 61 bitrd ( 𝜑 → ( ∃ 𝑑 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ∀ 𝑒 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 𝑑 ↔ ∃ 𝑓𝑎𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) )
63 9 inex1 ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ∈ V
64 63 a1i ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) → ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ∈ V )
65 6 sselda ( ( 𝜑𝑓𝑎 ) → 𝑓𝐴 )
66 1 2 3 fnwe2lem1 ( ( 𝜑𝑓𝐴 ) → ( 𝐹𝑓 ) / 𝑧 𝑆 We { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } )
67 wefr ( ( 𝐹𝑓 ) / 𝑧 𝑆 We { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } → ( 𝐹𝑓 ) / 𝑧 𝑆 Fr { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } )
68 66 67 syl ( ( 𝜑𝑓𝐴 ) → ( 𝐹𝑓 ) / 𝑧 𝑆 Fr { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } )
69 65 68 syldan ( ( 𝜑𝑓𝑎 ) → ( 𝐹𝑓 ) / 𝑧 𝑆 Fr { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } )
70 69 adantrr ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) → ( 𝐹𝑓 ) / 𝑧 𝑆 Fr { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } )
71 inss2 ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ⊆ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) }
72 71 a1i ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) → ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ⊆ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } )
73 simprl ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) → 𝑓𝑎 )
74 fveqeq2 ( 𝑦 = 𝑓 → ( ( 𝐹𝑦 ) = ( 𝐹𝑓 ) ↔ ( 𝐹𝑓 ) = ( 𝐹𝑓 ) ) )
75 65 adantrr ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) → 𝑓𝐴 )
76 eqidd ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) → ( 𝐹𝑓 ) = ( 𝐹𝑓 ) )
77 74 75 76 elrabd ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) → 𝑓 ∈ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } )
78 73 77 elind ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) → 𝑓 ∈ ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) )
79 78 ne0d ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) → ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ≠ ∅ )
80 fri ( ( ( ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ∈ V ∧ ( 𝐹𝑓 ) / 𝑧 𝑆 Fr { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ∧ ( ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ⊆ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ∧ ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ≠ ∅ ) ) → ∃ 𝑒 ∈ ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ∀ 𝑔 ∈ ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 )
81 64 70 72 79 80 syl22anc ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) → ∃ 𝑒 ∈ ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ∀ 𝑔 ∈ ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 )
82 elin ( 𝑒 ∈ ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ↔ ( 𝑒𝑎𝑒 ∈ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) )
83 fveqeq2 ( 𝑦 = 𝑒 → ( ( 𝐹𝑦 ) = ( 𝐹𝑓 ) ↔ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) )
84 83 elrab ( 𝑒 ∈ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ↔ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) )
85 84 anbi2i ( ( 𝑒𝑎𝑒 ∈ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ↔ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) )
86 82 85 bitri ( 𝑒 ∈ ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ↔ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) )
87 elin ( 𝑔 ∈ ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ↔ ( 𝑔𝑎𝑔 ∈ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) )
88 fveqeq2 ( 𝑦 = 𝑔 → ( ( 𝐹𝑦 ) = ( 𝐹𝑓 ) ↔ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) )
89 88 elrab ( 𝑔 ∈ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ↔ ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) )
90 89 anbi2i ( ( 𝑔𝑎𝑔 ∈ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ↔ ( 𝑔𝑎 ∧ ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) ) )
91 87 90 bitri ( 𝑔 ∈ ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ↔ ( 𝑔𝑎 ∧ ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) ) )
92 91 imbi1i ( ( 𝑔 ∈ ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ↔ ( ( 𝑔𝑎 ∧ ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) )
93 impexp ( ( ( 𝑔𝑎 ∧ ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ↔ ( 𝑔𝑎 → ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) )
94 92 93 bitri ( ( 𝑔 ∈ ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ↔ ( 𝑔𝑎 → ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) )
95 94 ralbii2 ( ∀ 𝑔 ∈ ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ↔ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) )
96 simplrl ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) → 𝑒𝑎 )
97 fveq2 ( 𝑑 = 𝑐 → ( 𝐹𝑑 ) = ( 𝐹𝑐 ) )
98 97 breq1d ( 𝑑 = 𝑐 → ( ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ↔ ( 𝐹𝑐 ) 𝑅 ( 𝐹𝑓 ) ) )
99 98 notbid ( 𝑑 = 𝑐 → ( ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ↔ ¬ ( 𝐹𝑐 ) 𝑅 ( 𝐹𝑓 ) ) )
100 simplrr ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) → ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) )
101 100 ad2antrr ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ 𝑐𝑎 ) → ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) )
102 simpr ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ 𝑐𝑎 ) → 𝑐𝑎 )
103 99 101 102 rspcdva ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ 𝑐𝑎 ) → ¬ ( 𝐹𝑐 ) 𝑅 ( 𝐹𝑓 ) )
104 simprrr ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) → ( 𝐹𝑒 ) = ( 𝐹𝑓 ) )
105 104 ad2antrr ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ 𝑐𝑎 ) → ( 𝐹𝑒 ) = ( 𝐹𝑓 ) )
106 105 breq2d ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ 𝑐𝑎 ) → ( ( 𝐹𝑐 ) 𝑅 ( 𝐹𝑒 ) ↔ ( 𝐹𝑐 ) 𝑅 ( 𝐹𝑓 ) ) )
107 103 106 mtbird ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ 𝑐𝑎 ) → ¬ ( 𝐹𝑐 ) 𝑅 ( 𝐹𝑒 ) )
108 6 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) → 𝑎𝐴 )
109 108 sselda ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ 𝑐𝑎 ) → 𝑐𝐴 )
110 109 adantrr ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ ( 𝑐𝑎 ∧ ( 𝐹𝑐 ) = ( 𝐹𝑒 ) ) ) → 𝑐𝐴 )
111 simprr ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ ( 𝑐𝑎 ∧ ( 𝐹𝑐 ) = ( 𝐹𝑒 ) ) ) → ( 𝐹𝑐 ) = ( 𝐹𝑒 ) )
112 104 ad2antrr ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ ( 𝑐𝑎 ∧ ( 𝐹𝑐 ) = ( 𝐹𝑒 ) ) ) → ( 𝐹𝑒 ) = ( 𝐹𝑓 ) )
113 111 112 eqtrd ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ ( 𝑐𝑎 ∧ ( 𝐹𝑐 ) = ( 𝐹𝑒 ) ) ) → ( 𝐹𝑐 ) = ( 𝐹𝑓 ) )
114 eleq1w ( 𝑔 = 𝑐 → ( 𝑔𝐴𝑐𝐴 ) )
115 fveqeq2 ( 𝑔 = 𝑐 → ( ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ↔ ( 𝐹𝑐 ) = ( 𝐹𝑓 ) ) )
116 114 115 anbi12d ( 𝑔 = 𝑐 → ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) ↔ ( 𝑐𝐴 ∧ ( 𝐹𝑐 ) = ( 𝐹𝑓 ) ) ) )
117 breq1 ( 𝑔 = 𝑐 → ( 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒𝑐 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) )
118 117 notbid ( 𝑔 = 𝑐 → ( ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ↔ ¬ 𝑐 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) )
119 116 118 imbi12d ( 𝑔 = 𝑐 → ( ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ↔ ( ( 𝑐𝐴 ∧ ( 𝐹𝑐 ) = ( 𝐹𝑓 ) ) → ¬ 𝑐 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) )
120 simplr ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ ( 𝑐𝑎 ∧ ( 𝐹𝑐 ) = ( 𝐹𝑒 ) ) ) → ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) )
121 simprl ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ ( 𝑐𝑎 ∧ ( 𝐹𝑐 ) = ( 𝐹𝑒 ) ) ) → 𝑐𝑎 )
122 119 120 121 rspcdva ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ ( 𝑐𝑎 ∧ ( 𝐹𝑐 ) = ( 𝐹𝑒 ) ) ) → ( ( 𝑐𝐴 ∧ ( 𝐹𝑐 ) = ( 𝐹𝑓 ) ) → ¬ 𝑐 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) )
123 110 113 122 mp2and ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ ( 𝑐𝑎 ∧ ( 𝐹𝑐 ) = ( 𝐹𝑒 ) ) ) → ¬ 𝑐 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 )
124 111 112 eqtr2d ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ ( 𝑐𝑎 ∧ ( 𝐹𝑐 ) = ( 𝐹𝑒 ) ) ) → ( 𝐹𝑓 ) = ( 𝐹𝑐 ) )
125 124 csbeq1d ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ ( 𝑐𝑎 ∧ ( 𝐹𝑐 ) = ( 𝐹𝑒 ) ) ) → ( 𝐹𝑓 ) / 𝑧 𝑆 = ( 𝐹𝑐 ) / 𝑧 𝑆 )
126 125 breqd ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ ( 𝑐𝑎 ∧ ( 𝐹𝑐 ) = ( 𝐹𝑒 ) ) ) → ( 𝑐 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒𝑐 ( 𝐹𝑐 ) / 𝑧 𝑆 𝑒 ) )
127 123 126 mtbid ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ ( 𝑐𝑎 ∧ ( 𝐹𝑐 ) = ( 𝐹𝑒 ) ) ) → ¬ 𝑐 ( 𝐹𝑐 ) / 𝑧 𝑆 𝑒 )
128 127 expr ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ 𝑐𝑎 ) → ( ( 𝐹𝑐 ) = ( 𝐹𝑒 ) → ¬ 𝑐 ( 𝐹𝑐 ) / 𝑧 𝑆 𝑒 ) )
129 imnan ( ( ( 𝐹𝑐 ) = ( 𝐹𝑒 ) → ¬ 𝑐 ( 𝐹𝑐 ) / 𝑧 𝑆 𝑒 ) ↔ ¬ ( ( 𝐹𝑐 ) = ( 𝐹𝑒 ) ∧ 𝑐 ( 𝐹𝑐 ) / 𝑧 𝑆 𝑒 ) )
130 128 129 sylib ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ 𝑐𝑎 ) → ¬ ( ( 𝐹𝑐 ) = ( 𝐹𝑒 ) ∧ 𝑐 ( 𝐹𝑐 ) / 𝑧 𝑆 𝑒 ) )
131 ioran ( ¬ ( ( 𝐹𝑐 ) 𝑅 ( 𝐹𝑒 ) ∨ ( ( 𝐹𝑐 ) = ( 𝐹𝑒 ) ∧ 𝑐 ( 𝐹𝑐 ) / 𝑧 𝑆 𝑒 ) ) ↔ ( ¬ ( 𝐹𝑐 ) 𝑅 ( 𝐹𝑒 ) ∧ ¬ ( ( 𝐹𝑐 ) = ( 𝐹𝑒 ) ∧ 𝑐 ( 𝐹𝑐 ) / 𝑧 𝑆 𝑒 ) ) )
132 107 130 131 sylanbrc ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ 𝑐𝑎 ) → ¬ ( ( 𝐹𝑐 ) 𝑅 ( 𝐹𝑒 ) ∨ ( ( 𝐹𝑐 ) = ( 𝐹𝑒 ) ∧ 𝑐 ( 𝐹𝑐 ) / 𝑧 𝑆 𝑒 ) ) )
133 1 2 fnwe2val ( 𝑐 𝑇 𝑒 ↔ ( ( 𝐹𝑐 ) 𝑅 ( 𝐹𝑒 ) ∨ ( ( 𝐹𝑐 ) = ( 𝐹𝑒 ) ∧ 𝑐 ( 𝐹𝑐 ) / 𝑧 𝑆 𝑒 ) ) )
134 132 133 sylnibr ( ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) ∧ 𝑐𝑎 ) → ¬ 𝑐 𝑇 𝑒 )
135 134 ralrimiva ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) → ∀ 𝑐𝑎 ¬ 𝑐 𝑇 𝑒 )
136 breq2 ( 𝑏 = 𝑒 → ( 𝑐 𝑇 𝑏𝑐 𝑇 𝑒 ) )
137 136 notbid ( 𝑏 = 𝑒 → ( ¬ 𝑐 𝑇 𝑏 ↔ ¬ 𝑐 𝑇 𝑒 ) )
138 137 ralbidv ( 𝑏 = 𝑒 → ( ∀ 𝑐𝑎 ¬ 𝑐 𝑇 𝑏 ↔ ∀ 𝑐𝑎 ¬ 𝑐 𝑇 𝑒 ) )
139 138 rspcev ( ( 𝑒𝑎 ∧ ∀ 𝑐𝑎 ¬ 𝑐 𝑇 𝑒 ) → ∃ 𝑏𝑎𝑐𝑎 ¬ 𝑐 𝑇 𝑏 )
140 96 135 139 syl2anc ( ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) ∧ ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) ) → ∃ 𝑏𝑎𝑐𝑎 ¬ 𝑐 𝑇 𝑏 )
141 140 ex ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) → ( ∀ 𝑔𝑎 ( ( 𝑔𝐴 ∧ ( 𝐹𝑔 ) = ( 𝐹𝑓 ) ) → ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 ) → ∃ 𝑏𝑎𝑐𝑎 ¬ 𝑐 𝑇 𝑏 ) )
142 95 141 syl5bi ( ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) ∧ ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) ) → ( ∀ 𝑔 ∈ ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 → ∃ 𝑏𝑎𝑐𝑎 ¬ 𝑐 𝑇 𝑏 ) )
143 142 ex ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) → ( ( 𝑒𝑎 ∧ ( 𝑒𝐴 ∧ ( 𝐹𝑒 ) = ( 𝐹𝑓 ) ) ) → ( ∀ 𝑔 ∈ ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 → ∃ 𝑏𝑎𝑐𝑎 ¬ 𝑐 𝑇 𝑏 ) ) )
144 86 143 syl5bi ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) → ( 𝑒 ∈ ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) → ( ∀ 𝑔 ∈ ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 → ∃ 𝑏𝑎𝑐𝑎 ¬ 𝑐 𝑇 𝑏 ) ) )
145 144 rexlimdv ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) → ( ∃ 𝑒 ∈ ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ∀ 𝑔 ∈ ( 𝑎 ∩ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑓 ) } ) ¬ 𝑔 ( 𝐹𝑓 ) / 𝑧 𝑆 𝑒 → ∃ 𝑏𝑎𝑐𝑎 ¬ 𝑐 𝑇 𝑏 ) )
146 81 145 mpd ( ( 𝜑 ∧ ( 𝑓𝑎 ∧ ∀ 𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) ) ) → ∃ 𝑏𝑎𝑐𝑎 ¬ 𝑐 𝑇 𝑏 )
147 146 rexlimdvaa ( 𝜑 → ( ∃ 𝑓𝑎𝑑𝑎 ¬ ( 𝐹𝑑 ) 𝑅 ( 𝐹𝑓 ) → ∃ 𝑏𝑎𝑐𝑎 ¬ 𝑐 𝑇 𝑏 ) )
148 62 147 sylbid ( 𝜑 → ( ∃ 𝑑 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ∀ 𝑒 ∈ ( ( 𝐹𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 𝑑 → ∃ 𝑏𝑎𝑐𝑎 ¬ 𝑐 𝑇 𝑏 ) )
149 28 148 mpd ( 𝜑 → ∃ 𝑏𝑎𝑐𝑎 ¬ 𝑐 𝑇 𝑏 )