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