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 dfss2 ⊢ ( 𝑎 ⊆ dom ( 𝐹 ↾ 𝐴 ) ↔ ( 𝑎 ∩ dom ( 𝐹 ↾ 𝐴 ) ) = 𝑎 )
21 19 20 sylib ⊢ ( 𝜑 → ( 𝑎 ∩ dom ( 𝐹 ↾ 𝐴 ) ) = 𝑎 )
22 17 21 eqtrid ⊢ ( 𝜑 → ( 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 bitrid ⊢ ( 𝜑 → ( ∃ 𝑑 ∈ ( ( 𝐹 ↾ 𝐴 ) “ 𝑎 ) ∀ 𝑒 ∈ ( ( 𝐹 ↾ 𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 𝑑 ↔ ∃ 𝑓 ∈ 𝑎 ∀ 𝑒 ∈ ( ( 𝐹 ↾ 𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ) )
40 29 raleqi ⊢ ( ∀ 𝑒 ∈ ( ( 𝐹 ↾ 𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ↔ ∀ 𝑒 ∈ ran ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ¬ 𝑒 𝑅 ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) )
41 breq1 ⊢ ( 𝑒 = ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ‘ 𝑑 ) → ( 𝑒 𝑅 ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ↔ ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ‘ 𝑑 ) 𝑅 ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ) )
42 41 notbid ⊢ ( 𝑒 = ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ‘ 𝑑 ) → ( ¬ 𝑒 𝑅 ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ↔ ¬ ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ‘ 𝑑 ) 𝑅 ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ) )
43 42 ralrn ⊢ ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) Fn 𝑎 → ( ∀ 𝑒 ∈ ran ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ¬ 𝑒 𝑅 ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ↔ ∀ 𝑑 ∈ 𝑎 ¬ ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ‘ 𝑑 ) 𝑅 ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ) )
44 33 43 syl ⊢ ( 𝜑 → ( ∀ 𝑒 ∈ ran ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ¬ 𝑒 𝑅 ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ↔ ∀ 𝑑 ∈ 𝑎 ¬ ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ‘ 𝑑 ) 𝑅 ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ) )
45 40 44 bitrid ⊢ ( 𝜑 → ( ∀ 𝑒 ∈ ( ( 𝐹 ↾ 𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ↔ ∀ 𝑑 ∈ 𝑎 ¬ ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ‘ 𝑑 ) 𝑅 ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑎 ) ‘ 𝑓 ) ) )
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 biimtrid ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑎 ∧ ∀ 𝑑 ∈ 𝑎 ¬ ( 𝐹 ‘ 𝑑 ) 𝑅 ( 𝐹 ‘ 𝑓 ) ) ) ∧ ( 𝑒 ∈ 𝑎 ∧ ( 𝑒 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑒 ) = ( 𝐹 ‘ 𝑓 ) ) ) ) → ( ∀ 𝑔 ∈ ( 𝑎 ∩ { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑓 ) } ) ¬ 𝑔 ⦋ ( 𝐹 ‘ 𝑓 ) / 𝑧 ⦌ 𝑆 𝑒 → ∃ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 ¬ 𝑐 𝑇 𝑏 ) )
143 142 ex ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑎 ∧ ∀ 𝑑 ∈ 𝑎 ¬ ( 𝐹 ‘ 𝑑 ) 𝑅 ( 𝐹 ‘ 𝑓 ) ) ) → ( ( 𝑒 ∈ 𝑎 ∧ ( 𝑒 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑒 ) = ( 𝐹 ‘ 𝑓 ) ) ) → ( ∀ 𝑔 ∈ ( 𝑎 ∩ { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑓 ) } ) ¬ 𝑔 ⦋ ( 𝐹 ‘ 𝑓 ) / 𝑧 ⦌ 𝑆 𝑒 → ∃ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 ¬ 𝑐 𝑇 𝑏 ) ) )
144 86 143 biimtrid ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑎 ∧ ∀ 𝑑 ∈ 𝑎 ¬ ( 𝐹 ‘ 𝑑 ) 𝑅 ( 𝐹 ‘ 𝑓 ) ) ) → ( 𝑒 ∈ ( 𝑎 ∩ { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑓 ) } ) → ( ∀ 𝑔 ∈ ( 𝑎 ∩ { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑓 ) } ) ¬ 𝑔 ⦋ ( 𝐹 ‘ 𝑓 ) / 𝑧 ⦌ 𝑆 𝑒 → ∃ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 ¬ 𝑐 𝑇 𝑏 ) ) )
145 144 rexlimdv ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑎 ∧ ∀ 𝑑 ∈ 𝑎 ¬ ( 𝐹 ‘ 𝑑 ) 𝑅 ( 𝐹 ‘ 𝑓 ) ) ) → ( ∃ 𝑒 ∈ ( 𝑎 ∩ { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑓 ) } ) ∀ 𝑔 ∈ ( 𝑎 ∩ { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑓 ) } ) ¬ 𝑔 ⦋ ( 𝐹 ‘ 𝑓 ) / 𝑧 ⦌ 𝑆 𝑒 → ∃ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 ¬ 𝑐 𝑇 𝑏 ) )
146 81 145 mpd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑎 ∧ ∀ 𝑑 ∈ 𝑎 ¬ ( 𝐹 ‘ 𝑑 ) 𝑅 ( 𝐹 ‘ 𝑓 ) ) ) → ∃ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 ¬ 𝑐 𝑇 𝑏 )
147 146 rexlimdvaa ⊢ ( 𝜑 → ( ∃ 𝑓 ∈ 𝑎 ∀ 𝑑 ∈ 𝑎 ¬ ( 𝐹 ‘ 𝑑 ) 𝑅 ( 𝐹 ‘ 𝑓 ) → ∃ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 ¬ 𝑐 𝑇 𝑏 ) )
148 62 147 sylbid ⊢ ( 𝜑 → ( ∃ 𝑑 ∈ ( ( 𝐹 ↾ 𝐴 ) “ 𝑎 ) ∀ 𝑒 ∈ ( ( 𝐹 ↾ 𝐴 ) “ 𝑎 ) ¬ 𝑒 𝑅 𝑑 → ∃ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 ¬ 𝑐 𝑇 𝑏 ) )
149 28 148 mpd ⊢ ( 𝜑 → ∃ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 ¬ 𝑐 𝑇 𝑏 )