This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wessf1ornlem

Description: Given a function F on a well-ordered domain A there exists a subset of A such that F restricted to such subset is injective and onto the range of F (without using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses wessf1ornlem.f ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
wessf1ornlem.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
wessf1ornlem.r ⊢ ( 𝜑 → 𝑅 We 𝐴 )
wessf1ornlem.g ⊢ 𝐺 = ( 𝑦 ∈ ran 𝐹 ↦ ( ℩ 𝑥 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ∀ 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ¬ 𝑧 𝑅 𝑥 ) )
Assertion wessf1ornlem ( 𝜑 → ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝐹 )

Proof

Step Hyp Ref Expression
1 wessf1ornlem.f ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2 wessf1ornlem.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 wessf1ornlem.r ⊢ ( 𝜑 → 𝑅 We 𝐴 )
4 wessf1ornlem.g ⊢ 𝐺 = ( 𝑦 ∈ ran 𝐹 ↦ ( ℩ 𝑥 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ∀ 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ¬ 𝑧 𝑅 𝑥 ) )
5 cnvimass ⊢ ( ◡ 𝐹 “ { 𝑢 } ) ⊆ dom 𝐹
6 1 fndmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
7 6 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → dom 𝐹 = 𝐴 )
8 5 7 sseqtrid ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → ( ◡ 𝐹 “ { 𝑢 } ) ⊆ 𝐴 )
9 3 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → 𝑅 We 𝐴 )
10 5 6 sseqtrid ⊢ ( 𝜑 → ( ◡ 𝐹 “ { 𝑢 } ) ⊆ 𝐴 )
11 2 10 ssexd ⊢ ( 𝜑 → ( ◡ 𝐹 “ { 𝑢 } ) ∈ V )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → ( ◡ 𝐹 “ { 𝑢 } ) ∈ V )
13 inisegn0 ⊢ ( 𝑢 ∈ ran 𝐹 ↔ ( ◡ 𝐹 “ { 𝑢 } ) ≠ ∅ )
14 13 biimpi ⊢ ( 𝑢 ∈ ran 𝐹 → ( ◡ 𝐹 “ { 𝑢 } ) ≠ ∅ )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → ( ◡ 𝐹 “ { 𝑢 } ) ≠ ∅ )
16 wereu ⊢ ( ( 𝑅 We 𝐴 ∧ ( ( ◡ 𝐹 “ { 𝑢 } ) ∈ V ∧ ( ◡ 𝐹 “ { 𝑢 } ) ⊆ 𝐴 ∧ ( ◡ 𝐹 “ { 𝑢 } ) ≠ ∅ ) ) → ∃! 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 )
17 9 12 8 15 16 syl13anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → ∃! 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 )
18 riotacl ⊢ ( ∃! 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 → ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) )
19 17 18 syl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) )
20 8 19 sseldd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ∈ 𝐴 )
21 20 ralrimiva ⊢ ( 𝜑 → ∀ 𝑢 ∈ ran 𝐹 ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ∈ 𝐴 )
22 sneq ⊢ ( 𝑦 = 𝑢 → { 𝑦 } = { 𝑢 } )
23 22 imaeq2d ⊢ ( 𝑦 = 𝑢 → ( ◡ 𝐹 “ { 𝑦 } ) = ( ◡ 𝐹 “ { 𝑢 } ) )
24 23 raleqdv ⊢ ( 𝑦 = 𝑢 → ( ∀ 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ¬ 𝑧 𝑅 𝑥 ↔ ∀ 𝑧 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑧 𝑅 𝑥 ) )
25 23 24 riotaeqbidv ⊢ ( 𝑦 = 𝑢 → ( ℩ 𝑥 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ∀ 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ¬ 𝑧 𝑅 𝑥 ) = ( ℩ 𝑥 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑧 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑧 𝑅 𝑥 ) )
26 breq1 ⊢ ( 𝑧 = 𝑡 → ( 𝑧 𝑅 𝑥 ↔ 𝑡 𝑅 𝑥 ) )
27 26 notbid ⊢ ( 𝑧 = 𝑡 → ( ¬ 𝑧 𝑅 𝑥 ↔ ¬ 𝑡 𝑅 𝑥 ) )
28 27 cbvralvw ⊢ ( ∀ 𝑧 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑧 𝑅 𝑥 ↔ ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑥 )
29 breq2 ⊢ ( 𝑥 = 𝑣 → ( 𝑡 𝑅 𝑥 ↔ 𝑡 𝑅 𝑣 ) )
30 29 notbid ⊢ ( 𝑥 = 𝑣 → ( ¬ 𝑡 𝑅 𝑥 ↔ ¬ 𝑡 𝑅 𝑣 ) )
31 30 ralbidv ⊢ ( 𝑥 = 𝑣 → ( ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑥 ↔ ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) )
32 28 31 bitrid ⊢ ( 𝑥 = 𝑣 → ( ∀ 𝑧 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑧 𝑅 𝑥 ↔ ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) )
33 32 cbvriotavw ⊢ ( ℩ 𝑥 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑧 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑧 𝑅 𝑥 ) = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 )
34 25 33 eqtrdi ⊢ ( 𝑦 = 𝑢 → ( ℩ 𝑥 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ∀ 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ¬ 𝑧 𝑅 𝑥 ) = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) )
35 34 cbvmptv ⊢ ( 𝑦 ∈ ran 𝐹 ↦ ( ℩ 𝑥 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ∀ 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ¬ 𝑧 𝑅 𝑥 ) ) = ( 𝑢 ∈ ran 𝐹 ↦ ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) )
36 4 35 eqtri ⊢ 𝐺 = ( 𝑢 ∈ ran 𝐹 ↦ ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) )
37 36 rnmptss ⊢ ( ∀ 𝑢 ∈ ran 𝐹 ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ∈ 𝐴 → ran 𝐺 ⊆ 𝐴 )
38 21 37 syl ⊢ ( 𝜑 → ran 𝐺 ⊆ 𝐴 )
39 2 38 sselpwd ⊢ ( 𝜑 → ran 𝐺 ∈ 𝒫 𝐴 )
40 dffn3 ⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 ⟶ ran 𝐹 )
41 1 40 sylib ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ran 𝐹 )
42 41 38 fssresd ⊢ ( 𝜑 → ( 𝐹 ↾ ran 𝐺 ) : ran 𝐺 ⟶ ran 𝐹 )
43 fvres ⊢ ( 𝑤 ∈ ran 𝐺 → ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
44 43 eqcomd ⊢ ( 𝑤 ∈ ran 𝐺 → ( 𝐹 ‘ 𝑤 ) = ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑤 ) )
45 44 ad2antrr ⊢ ( ( ( 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑤 ) = ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑡 ) ) → ( 𝐹 ‘ 𝑤 ) = ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑤 ) )
46 simpr ⊢ ( ( ( 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑤 ) = ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑡 ) ) → ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑤 ) = ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑡 ) )
47 fvres ⊢ ( 𝑡 ∈ ran 𝐺 → ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑡 ) = ( 𝐹 ‘ 𝑡 ) )
48 47 ad2antlr ⊢ ( ( ( 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑤 ) = ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑡 ) ) → ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑡 ) = ( 𝐹 ‘ 𝑡 ) )
49 45 46 48 3eqtrd ⊢ ( ( ( 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑤 ) = ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑡 ) ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) )
50 49 3adantl1 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑤 ) = ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑡 ) ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) )
51 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) → 𝜑 )
52 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) → 𝑡 ∈ ran 𝐺 )
53 simpl2 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) → 𝑤 ∈ ran 𝐺 )
54 id ⊢ ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) )
55 54 eqcomd ⊢ ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑤 ) )
56 55 adantl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑤 ) )
57 eleq1w ⊢ ( 𝑏 = 𝑤 → ( 𝑏 ∈ ran 𝐺 ↔ 𝑤 ∈ ran 𝐺 ) )
58 57 3anbi3d ⊢ ( 𝑏 = 𝑤 → ( ( 𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺 ) ↔ ( 𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑤 ∈ ran 𝐺 ) ) )
59 fveq2 ⊢ ( 𝑏 = 𝑤 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑤 ) )
60 59 eqeq2d ⊢ ( 𝑏 = 𝑤 → ( ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑏 ) ↔ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑤 ) ) )
61 58 60 anbi12d ⊢ ( 𝑏 = 𝑤 → ( ( ( 𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑏 ) ) ↔ ( ( 𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑤 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑤 ) ) ) )
62 breq1 ⊢ ( 𝑏 = 𝑤 → ( 𝑏 𝑅 𝑡 ↔ 𝑤 𝑅 𝑡 ) )
63 62 notbid ⊢ ( 𝑏 = 𝑤 → ( ¬ 𝑏 𝑅 𝑡 ↔ ¬ 𝑤 𝑅 𝑡 ) )
64 61 63 imbi12d ⊢ ( 𝑏 = 𝑤 → ( ( ( ( 𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑏 ) ) → ¬ 𝑏 𝑅 𝑡 ) ↔ ( ( ( 𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑤 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑤 ) ) → ¬ 𝑤 𝑅 𝑡 ) ) )
65 eleq1w ⊢ ( 𝑎 = 𝑡 → ( 𝑎 ∈ ran 𝐺 ↔ 𝑡 ∈ ran 𝐺 ) )
66 65 3anbi2d ⊢ ( 𝑎 = 𝑡 → ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺 ) ↔ ( 𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺 ) ) )
67 fveqeq2 ⊢ ( 𝑎 = 𝑡 → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ↔ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑏 ) ) )
68 66 67 anbi12d ⊢ ( 𝑎 = 𝑡 → ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ↔ ( ( 𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑏 ) ) ) )
69 breq2 ⊢ ( 𝑎 = 𝑡 → ( 𝑏 𝑅 𝑎 ↔ 𝑏 𝑅 𝑡 ) )
70 69 notbid ⊢ ( 𝑎 = 𝑡 → ( ¬ 𝑏 𝑅 𝑎 ↔ ¬ 𝑏 𝑅 𝑡 ) )
71 68 70 imbi12d ⊢ ( 𝑎 = 𝑡 → ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) → ¬ 𝑏 𝑅 𝑎 ) ↔ ( ( ( 𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑏 ) ) → ¬ 𝑏 𝑅 𝑡 ) ) )
72 eleq1w ⊢ ( 𝑡 = 𝑏 → ( 𝑡 ∈ ran 𝐺 ↔ 𝑏 ∈ ran 𝐺 ) )
73 72 3anbi3d ⊢ ( 𝑡 = 𝑏 → ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ↔ ( 𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺 ) ) )
74 fveq2 ⊢ ( 𝑡 = 𝑏 → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑏 ) )
75 74 eqeq2d ⊢ ( 𝑡 = 𝑏 → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑡 ) ↔ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) )
76 73 75 anbi12d ⊢ ( 𝑡 = 𝑏 → ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑡 ) ) ↔ ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ) )
77 breq1 ⊢ ( 𝑡 = 𝑏 → ( 𝑡 𝑅 𝑎 ↔ 𝑏 𝑅 𝑎 ) )
78 77 notbid ⊢ ( 𝑡 = 𝑏 → ( ¬ 𝑡 𝑅 𝑎 ↔ ¬ 𝑏 𝑅 𝑎 ) )
79 76 78 imbi12d ⊢ ( 𝑡 = 𝑏 → ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑡 ) ) → ¬ 𝑡 𝑅 𝑎 ) ↔ ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) → ¬ 𝑏 𝑅 𝑎 ) ) )
80 eleq1w ⊢ ( 𝑤 = 𝑎 → ( 𝑤 ∈ ran 𝐺 ↔ 𝑎 ∈ ran 𝐺 ) )
81 80 3anbi2d ⊢ ( 𝑤 = 𝑎 → ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ↔ ( 𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ) )
82 fveqeq2 ⊢ ( 𝑤 = 𝑎 → ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ↔ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑡 ) ) )
83 81 82 anbi12d ⊢ ( 𝑤 = 𝑎 → ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) ↔ ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑡 ) ) ) )
84 breq2 ⊢ ( 𝑤 = 𝑎 → ( 𝑡 𝑅 𝑤 ↔ 𝑡 𝑅 𝑎 ) )
85 84 notbid ⊢ ( 𝑤 = 𝑎 → ( ¬ 𝑡 𝑅 𝑤 ↔ ¬ 𝑡 𝑅 𝑎 ) )
86 83 85 imbi12d ⊢ ( 𝑤 = 𝑎 → ( ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) → ¬ 𝑡 𝑅 𝑤 ) ↔ ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑡 ) ) → ¬ 𝑡 𝑅 𝑎 ) ) )
87 36 elrnmpt ⊢ ( 𝑤 ∈ V → ( 𝑤 ∈ ran 𝐺 ↔ ∃ 𝑢 ∈ ran 𝐹 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) )
88 87 elv ⊢ ( 𝑤 ∈ ran 𝐺 ↔ ∃ 𝑢 ∈ ran 𝐹 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) )
89 88 biimpi ⊢ ( 𝑤 ∈ ran 𝐺 → ∃ 𝑢 ∈ ran 𝐹 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) )
90 89 adantr ⊢ ( ( 𝑤 ∈ ran 𝐺 ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) → ∃ 𝑢 ∈ ran 𝐹 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) )
91 90 3ad2antl2 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) → ∃ 𝑢 ∈ ran 𝐹 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) )
92 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) )
93 92 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) = 𝑤 )
94 simp11 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → 𝜑 )
95 id ⊢ ( 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) → 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) )
96 breq2 ⊢ ( 𝑣 = 𝑤 → ( 𝑡 𝑅 𝑣 ↔ 𝑡 𝑅 𝑤 ) )
97 96 notbid ⊢ ( 𝑣 = 𝑤 → ( ¬ 𝑡 𝑅 𝑣 ↔ ¬ 𝑡 𝑅 𝑤 ) )
98 97 ralbidv ⊢ ( 𝑣 = 𝑤 → ( ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ↔ ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑤 ) )
99 98 cbvriotavw ⊢ ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) = ( ℩ 𝑤 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑤 )
100 95 99 eqtr2di ⊢ ( 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) → ( ℩ 𝑤 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑤 ) = 𝑤 )
101 100 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → ( ℩ 𝑤 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑤 ) = 𝑤 )
102 98 cbvreuvw ⊢ ( ∃! 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ↔ ∃! 𝑤 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑤 )
103 17 102 sylib ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → ∃! 𝑤 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑤 )
104 riota1 ⊢ ( ∃! 𝑤 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑤 → ( ( 𝑤 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∧ ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑤 ) ↔ ( ℩ 𝑤 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑤 ) = 𝑤 ) )
105 103 104 syl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → ( ( 𝑤 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∧ ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑤 ) ↔ ( ℩ 𝑤 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑤 ) = 𝑤 ) )
106 105 3adant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → ( ( 𝑤 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∧ ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑤 ) ↔ ( ℩ 𝑤 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑤 ) = 𝑤 ) )
107 101 106 mpbird ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → ( 𝑤 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∧ ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑤 ) )
108 107 simpld ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → 𝑤 ∈ ( ◡ 𝐹 “ { 𝑢 } ) )
109 94 108 syld3an1 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → 𝑤 ∈ ( ◡ 𝐹 “ { 𝑢 } ) )
110 simp2 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → 𝑢 ∈ ran 𝐹 )
111 94 110 17 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → ∃! 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 )
112 98 riota2 ⊢ ( ( 𝑤 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∧ ∃! 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) → ( ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑤 ↔ ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) = 𝑤 ) )
113 109 111 112 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → ( ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑤 ↔ ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) = 𝑤 ) )
114 93 113 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑤 )
115 114 3adant1r ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑤 )
116 38 sselda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ran 𝐺 ) → 𝑡 ∈ 𝐴 )
117 116 3adant2 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) → 𝑡 ∈ 𝐴 )
118 117 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) → 𝑡 ∈ 𝐴 )
119 118 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → 𝑡 ∈ 𝐴 )
120 55 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) ∧ 𝑢 ∈ ran 𝐹 ) → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑤 ) )
121 120 3adant3 ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑤 ) )
122 fniniseg ⊢ ( 𝐹 Fn 𝐴 → ( 𝑤 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ( 𝑤 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑢 ) ) )
123 94 1 122 3syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → ( 𝑤 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ( 𝑤 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑢 ) ) )
124 109 123 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → ( 𝑤 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑢 ) )
125 124 simprd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → ( 𝐹 ‘ 𝑤 ) = 𝑢 )
126 125 3adant1r ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → ( 𝐹 ‘ 𝑤 ) = 𝑢 )
127 121 126 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → ( 𝐹 ‘ 𝑡 ) = 𝑢 )
128 fniniseg ⊢ ( 𝐹 Fn 𝐴 → ( 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ( 𝑡 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑢 ) ) )
129 1 128 syl ⊢ ( 𝜑 → ( 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ( 𝑡 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑢 ) ) )
130 129 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) → ( 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ( 𝑡 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑢 ) ) )
131 130 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) ∧ 𝑢 ∈ ran 𝐹 ) → ( 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ( 𝑡 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑢 ) ) )
132 131 3adant3 ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → ( 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ( 𝑡 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑡 ) = 𝑢 ) ) )
133 119 127 132 mpbir2and ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) )
134 rspa ⊢ ( ( ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑤 ∧ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ) → ¬ 𝑡 𝑅 𝑤 )
135 115 133 134 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ) → ¬ 𝑡 𝑅 𝑤 )
136 135 rexlimdv3a ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) → ( ∃ 𝑢 ∈ ran 𝐹 𝑤 = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) → ¬ 𝑡 𝑅 𝑤 ) )
137 91 136 mpd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) → ¬ 𝑡 𝑅 𝑤 )
138 86 137 chvarvv ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑡 ) ) → ¬ 𝑡 𝑅 𝑎 )
139 79 138 chvarvv ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) → ¬ 𝑏 𝑅 𝑎 )
140 71 139 chvarvv ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑏 ) ) → ¬ 𝑏 𝑅 𝑡 )
141 64 140 chvarvv ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑤 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑤 ) ) → ¬ 𝑤 𝑅 𝑡 )
142 51 52 53 56 141 syl31anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) → ¬ 𝑤 𝑅 𝑡 )
143 weso ⊢ ( 𝑅 We 𝐴 → 𝑅 Or 𝐴 )
144 3 143 syl ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
145 144 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) → 𝑅 Or 𝐴 )
146 145 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) → 𝑅 Or 𝐴 )
147 38 sselda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ) → 𝑤 ∈ 𝐴 )
148 147 3adant3 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) → 𝑤 ∈ 𝐴 )
149 148 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) → 𝑤 ∈ 𝐴 )
150 sotrieq2 ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ) → ( 𝑤 = 𝑡 ↔ ( ¬ 𝑤 𝑅 𝑡 ∧ ¬ 𝑡 𝑅 𝑤 ) ) )
151 146 149 118 150 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) → ( 𝑤 = 𝑡 ↔ ( ¬ 𝑤 𝑅 𝑡 ∧ ¬ 𝑡 𝑅 𝑤 ) ) )
152 142 137 151 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) ) → 𝑤 = 𝑡 )
153 50 152 syldan ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ∧ ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑤 ) = ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑡 ) ) → 𝑤 = 𝑡 )
154 153 ex ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) → ( ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑤 ) = ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑡 ) → 𝑤 = 𝑡 ) )
155 154 3expb ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺 ) ) → ( ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑤 ) = ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑡 ) → 𝑤 = 𝑡 ) )
156 155 ralrimivva ⊢ ( 𝜑 → ∀ 𝑤 ∈ ran 𝐺 ∀ 𝑡 ∈ ran 𝐺 ( ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑤 ) = ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑡 ) → 𝑤 = 𝑡 ) )
157 dff13 ⊢ ( ( 𝐹 ↾ ran 𝐺 ) : ran 𝐺 –1-1→ ran 𝐹 ↔ ( ( 𝐹 ↾ ran 𝐺 ) : ran 𝐺 ⟶ ran 𝐹 ∧ ∀ 𝑤 ∈ ran 𝐺 ∀ 𝑡 ∈ ran 𝐺 ( ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑤 ) = ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑡 ) → 𝑤 = 𝑡 ) ) )
158 42 156 157 sylanbrc ⊢ ( 𝜑 → ( 𝐹 ↾ ran 𝐺 ) : ran 𝐺 –1-1→ ran 𝐹 )
159 riotaex ⊢ ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ∈ V
160 159 rgenw ⊢ ∀ 𝑢 ∈ ran 𝐹 ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ∈ V
161 36 fnmpt ⊢ ( ∀ 𝑢 ∈ ran 𝐹 ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ∈ V → 𝐺 Fn ran 𝐹 )
162 160 161 mp1i ⊢ ( 𝜑 → 𝐺 Fn ran 𝐹 )
163 dffn3 ⊢ ( 𝐺 Fn ran 𝐹 ↔ 𝐺 : ran 𝐹 ⟶ ran 𝐺 )
164 162 163 sylib ⊢ ( 𝜑 → 𝐺 : ran 𝐹 ⟶ ran 𝐺 )
165 164 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → ( 𝐺 ‘ 𝑢 ) ∈ ran 𝐺 )
166 165 fvresd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → ( ( 𝐹 ↾ ran 𝐺 ) ‘ ( 𝐺 ‘ 𝑢 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) )
167 simpr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → 𝑢 ∈ ran 𝐹 )
168 159 a1i ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) ∈ V )
169 4 34 167 168 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → ( 𝐺 ‘ 𝑢 ) = ( ℩ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ∀ 𝑡 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ¬ 𝑡 𝑅 𝑣 ) )
170 169 19 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → ( 𝐺 ‘ 𝑢 ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) )
171 fvex ⊢ ( 𝐺 ‘ 𝑢 ) ∈ V
172 eleq1 ⊢ ( 𝑤 = ( 𝐺 ‘ 𝑢 ) → ( 𝑤 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ( 𝐺 ‘ 𝑢 ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ) )
173 eleq1 ⊢ ( 𝑤 = ( 𝐺 ‘ 𝑢 ) → ( 𝑤 ∈ 𝐴 ↔ ( 𝐺 ‘ 𝑢 ) ∈ 𝐴 ) )
174 fveqeq2 ⊢ ( 𝑤 = ( 𝐺 ‘ 𝑢 ) → ( ( 𝐹 ‘ 𝑤 ) = 𝑢 ↔ ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) = 𝑢 ) )
175 173 174 anbi12d ⊢ ( 𝑤 = ( 𝐺 ‘ 𝑢 ) → ( ( 𝑤 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑢 ) ↔ ( ( 𝐺 ‘ 𝑢 ) ∈ 𝐴 ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) = 𝑢 ) ) )
176 172 175 bibi12d ⊢ ( 𝑤 = ( 𝐺 ‘ 𝑢 ) → ( ( 𝑤 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ( 𝑤 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑢 ) ) ↔ ( ( 𝐺 ‘ 𝑢 ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ( ( 𝐺 ‘ 𝑢 ) ∈ 𝐴 ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) = 𝑢 ) ) ) )
177 176 imbi2d ⊢ ( 𝑤 = ( 𝐺 ‘ 𝑢 ) → ( ( 𝜑 → ( 𝑤 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ( 𝑤 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑢 ) ) ) ↔ ( 𝜑 → ( ( 𝐺 ‘ 𝑢 ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ( ( 𝐺 ‘ 𝑢 ) ∈ 𝐴 ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) = 𝑢 ) ) ) ) )
178 1 122 syl ⊢ ( 𝜑 → ( 𝑤 ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ( 𝑤 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑢 ) ) )
179 171 177 178 vtocl ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑢 ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ( ( 𝐺 ‘ 𝑢 ) ∈ 𝐴 ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) = 𝑢 ) ) )
180 179 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → ( ( 𝐺 ‘ 𝑢 ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ( ( 𝐺 ‘ 𝑢 ) ∈ 𝐴 ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) = 𝑢 ) ) )
181 170 180 mpbid ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → ( ( 𝐺 ‘ 𝑢 ) ∈ 𝐴 ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) = 𝑢 ) )
182 181 simprd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) = 𝑢 )
183 166 182 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → 𝑢 = ( ( 𝐹 ↾ ran 𝐺 ) ‘ ( 𝐺 ‘ 𝑢 ) ) )
184 fveq2 ⊢ ( 𝑤 = ( 𝐺 ‘ 𝑢 ) → ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑤 ) = ( ( 𝐹 ↾ ran 𝐺 ) ‘ ( 𝐺 ‘ 𝑢 ) ) )
185 184 rspceeqv ⊢ ( ( ( 𝐺 ‘ 𝑢 ) ∈ ran 𝐺 ∧ 𝑢 = ( ( 𝐹 ↾ ran 𝐺 ) ‘ ( 𝐺 ‘ 𝑢 ) ) ) → ∃ 𝑤 ∈ ran 𝐺 𝑢 = ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑤 ) )
186 165 183 185 syl2anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ran 𝐹 ) → ∃ 𝑤 ∈ ran 𝐺 𝑢 = ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑤 ) )
187 186 ralrimiva ⊢ ( 𝜑 → ∀ 𝑢 ∈ ran 𝐹 ∃ 𝑤 ∈ ran 𝐺 𝑢 = ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑤 ) )
188 dffo3 ⊢ ( ( 𝐹 ↾ ran 𝐺 ) : ran 𝐺 –onto→ ran 𝐹 ↔ ( ( 𝐹 ↾ ran 𝐺 ) : ran 𝐺 ⟶ ran 𝐹 ∧ ∀ 𝑢 ∈ ran 𝐹 ∃ 𝑤 ∈ ran 𝐺 𝑢 = ( ( 𝐹 ↾ ran 𝐺 ) ‘ 𝑤 ) ) )
189 42 187 188 sylanbrc ⊢ ( 𝜑 → ( 𝐹 ↾ ran 𝐺 ) : ran 𝐺 –onto→ ran 𝐹 )
190 df-f1o ⊢ ( ( 𝐹 ↾ ran 𝐺 ) : ran 𝐺 –1-1-onto→ ran 𝐹 ↔ ( ( 𝐹 ↾ ran 𝐺 ) : ran 𝐺 –1-1→ ran 𝐹 ∧ ( 𝐹 ↾ ran 𝐺 ) : ran 𝐺 –onto→ ran 𝐹 ) )
191 158 189 190 sylanbrc ⊢ ( 𝜑 → ( 𝐹 ↾ ran 𝐺 ) : ran 𝐺 –1-1-onto→ ran 𝐹 )
192 reseq2 ⊢ ( 𝑣 = ran 𝐺 → ( 𝐹 ↾ 𝑣 ) = ( 𝐹 ↾ ran 𝐺 ) )
193 id ⊢ ( 𝑣 = ran 𝐺 → 𝑣 = ran 𝐺 )
194 eqidd ⊢ ( 𝑣 = ran 𝐺 → ran 𝐹 = ran 𝐹 )
195 192 193 194 f1oeq123d ⊢ ( 𝑣 = ran 𝐺 → ( ( 𝐹 ↾ 𝑣 ) : 𝑣 –1-1-onto→ ran 𝐹 ↔ ( 𝐹 ↾ ran 𝐺 ) : ran 𝐺 –1-1-onto→ ran 𝐹 ) )
196 195 rspcev ⊢ ( ( ran 𝐺 ∈ 𝒫 𝐴 ∧ ( 𝐹 ↾ ran 𝐺 ) : ran 𝐺 –1-1-onto→ ran 𝐹 ) → ∃ 𝑣 ∈ 𝒫 𝐴 ( 𝐹 ↾ 𝑣 ) : 𝑣 –1-1-onto→ ran 𝐹 )
197 39 191 196 syl2anc ⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝒫 𝐴 ( 𝐹 ↾ 𝑣 ) : 𝑣 –1-1-onto→ ran 𝐹 )
198 reseq2 ⊢ ( 𝑣 = 𝑥 → ( 𝐹 ↾ 𝑣 ) = ( 𝐹 ↾ 𝑥 ) )
199 id ⊢ ( 𝑣 = 𝑥 → 𝑣 = 𝑥 )
200 eqidd ⊢ ( 𝑣 = 𝑥 → ran 𝐹 = ran 𝐹 )
201 198 199 200 f1oeq123d ⊢ ( 𝑣 = 𝑥 → ( ( 𝐹 ↾ 𝑣 ) : 𝑣 –1-1-onto→ ran 𝐹 ↔ ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝐹 ) )
202 201 cbvrexvw ⊢ ( ∃ 𝑣 ∈ 𝒫 𝐴 ( 𝐹 ↾ 𝑣 ) : 𝑣 –1-1-onto→ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝐹 )
203 197 202 sylib ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝐹 )