Metamath Proof Explorer

Theorem fnwe2lem3

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 𝐵 )
fnwe2lem3.a ⊢ ( 𝜑 → 𝑎 ⊆ 𝐴 )
fnwe2lem3.n0 ⊢ ( 𝜑 → 𝑎 ≠ ∅ )
Assertion fnwe2lem3 ( 𝜑 → ∃ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 ¬ 𝑐 𝑇 𝑏 )

Proof

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