Metamath Proof Explorer

Theorem uspgrsprfo

Description: The mapping F is a function from the "simple pseudographs" with a fixed set of vertices V onto the subsets of the set of pairs over the set V . (Contributed by AV, 25-Nov-2021)

Ref Expression
Hypotheses uspgrsprf.p ⊢ 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
uspgrsprf.g ⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) }
uspgrsprf.f ⊢ 𝐹 = ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) )
Assertion uspgrsprfo ( 𝑉 ∈ 𝑊 → 𝐹 : 𝐺 –onto→ 𝑃 )

Proof

Step Hyp Ref Expression
1 uspgrsprf.p ⊢ 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
2 uspgrsprf.g ⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) }
3 uspgrsprf.f ⊢ 𝐹 = ( 𝑔 ∈ 𝐺 ↦ ( 2nd ‘ 𝑔 ) )
4 1 2 3 uspgrsprf ⊢ 𝐹 : 𝐺 ⟶ 𝑃
5 4 a1i ⊢ ( 𝑉 ∈ 𝑊 → 𝐹 : 𝐺 ⟶ 𝑃 )
6 1 eleq2i ⊢ ( 𝑎 ∈ 𝑃 ↔ 𝑎 ∈ 𝒫 ( Pairs ‘ 𝑉 ) )
7 velpw ⊢ ( 𝑎 ∈ 𝒫 ( Pairs ‘ 𝑉 ) ↔ 𝑎 ⊆ ( Pairs ‘ 𝑉 ) )
8 6 7 bitri ⊢ ( 𝑎 ∈ 𝑃 ↔ 𝑎 ⊆ ( Pairs ‘ 𝑉 ) )
9 eqidd ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) → 𝑉 = 𝑉 )
10 vex ⊢ 𝑎 ∈ V
11 10 a1i ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) → 𝑎 ∈ V )
12 f1oi ⊢ ( I ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝑎
13 12 a1i ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) → ( I ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝑎 )
14 dmresi ⊢ dom ( I ↾ 𝑎 ) = 𝑎
15 f1oeq2 ⊢ ( dom ( I ↾ 𝑎 ) = 𝑎 → ( ( I ↾ 𝑎 ) : dom ( I ↾ 𝑎 ) –1-1-onto→ 𝑎 ↔ ( I ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝑎 ) )
16 14 15 ax-mp ⊢ ( ( I ↾ 𝑎 ) : dom ( I ↾ 𝑎 ) –1-1-onto→ 𝑎 ↔ ( I ↾ 𝑎 ) : 𝑎 –1-1-onto→ 𝑎 )
17 13 16 sylibr ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) → ( I ↾ 𝑎 ) : dom ( I ↾ 𝑎 ) –1-1-onto→ 𝑎 )
18 sprvalpwle2 ⊢ ( 𝑉 ∈ 𝑊 → ( Pairs ‘ 𝑉 ) = { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } )
19 18 sseq2d ⊢ ( 𝑉 ∈ 𝑊 → ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ↔ 𝑎 ⊆ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
20 19 biimpac ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) → 𝑎 ⊆ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } )
21 17 20 jca ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) → ( ( I ↾ 𝑎 ) : dom ( I ↾ 𝑎 ) –1-1-onto→ 𝑎 ∧ 𝑎 ⊆ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
22 f1oeq3 ⊢ ( 𝑓 = 𝑎 → ( ( I ↾ 𝑎 ) : dom ( I ↾ 𝑎 ) –1-1-onto→ 𝑓 ↔ ( I ↾ 𝑎 ) : dom ( I ↾ 𝑎 ) –1-1-onto→ 𝑎 ) )
23 sseq1 ⊢ ( 𝑓 = 𝑎 → ( 𝑓 ⊆ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ↔ 𝑎 ⊆ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
24 22 23 anbi12d ⊢ ( 𝑓 = 𝑎 → ( ( ( I ↾ 𝑎 ) : dom ( I ↾ 𝑎 ) –1-1-onto→ 𝑓 ∧ 𝑓 ⊆ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) ↔ ( ( I ↾ 𝑎 ) : dom ( I ↾ 𝑎 ) –1-1-onto→ 𝑎 ∧ 𝑎 ⊆ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) ) )
25 11 21 24 spcedv ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) → ∃ 𝑓 ( ( I ↾ 𝑎 ) : dom ( I ↾ 𝑎 ) –1-1-onto→ 𝑓 ∧ 𝑓 ⊆ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
26 resiexg ⊢ ( 𝑎 ∈ V → ( I ↾ 𝑎 ) ∈ V )
27 10 26 ax-mp ⊢ ( I ↾ 𝑎 ) ∈ V
28 27 f11o ⊢ ( ( I ↾ 𝑎 ) : dom ( I ↾ 𝑎 ) –1-1→ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ↔ ∃ 𝑓 ( ( I ↾ 𝑎 ) : dom ( I ↾ 𝑎 ) –1-1-onto→ 𝑓 ∧ 𝑓 ⊆ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
29 25 28 sylibr ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) → ( I ↾ 𝑎 ) : dom ( I ↾ 𝑎 ) –1-1→ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } )
30 10 a1i ⊢ ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) → 𝑎 ∈ V )
31 30 resiexd ⊢ ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) → ( I ↾ 𝑎 ) ∈ V )
32 31 anim1ci ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) → ( 𝑉 ∈ 𝑊 ∧ ( I ↾ 𝑎 ) ∈ V ) )
33 isuspgrop ⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( I ↾ 𝑎 ) ∈ V ) → ( ⟨ 𝑉 , ( I ↾ 𝑎 ) ⟩ ∈ USPGraph ↔ ( I ↾ 𝑎 ) : dom ( I ↾ 𝑎 ) –1-1→ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
34 32 33 syl ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) → ( ⟨ 𝑉 , ( I ↾ 𝑎 ) ⟩ ∈ USPGraph ↔ ( I ↾ 𝑎 ) : dom ( I ↾ 𝑎 ) –1-1→ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
35 29 34 mpbird ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) → ⟨ 𝑉 , ( I ↾ 𝑎 ) ⟩ ∈ USPGraph )
36 fveqeq2 ⊢ ( 𝑞 = ⟨ 𝑉 , ( I ↾ 𝑎 ) ⟩ → ( ( Vtx ‘ 𝑞 ) = 𝑉 ↔ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑎 ) ⟩ ) = 𝑉 ) )
37 fveqeq2 ⊢ ( 𝑞 = ⟨ 𝑉 , ( I ↾ 𝑎 ) ⟩ → ( ( Edg ‘ 𝑞 ) = 𝑎 ↔ ( Edg ‘ ⟨ 𝑉 , ( I ↾ 𝑎 ) ⟩ ) = 𝑎 ) )
38 36 37 anbi12d ⊢ ( 𝑞 = ⟨ 𝑉 , ( I ↾ 𝑎 ) ⟩ → ( ( ( Vtx ‘ 𝑞 ) = 𝑉 ∧ ( Edg ‘ 𝑞 ) = 𝑎 ) ↔ ( ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑎 ) ⟩ ) = 𝑉 ∧ ( Edg ‘ ⟨ 𝑉 , ( I ↾ 𝑎 ) ⟩ ) = 𝑎 ) ) )
39 38 adantl ⊢ ( ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) ∧ 𝑞 = ⟨ 𝑉 , ( I ↾ 𝑎 ) ⟩ ) → ( ( ( Vtx ‘ 𝑞 ) = 𝑉 ∧ ( Edg ‘ 𝑞 ) = 𝑎 ) ↔ ( ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑎 ) ⟩ ) = 𝑉 ∧ ( Edg ‘ ⟨ 𝑉 , ( I ↾ 𝑎 ) ⟩ ) = 𝑎 ) ) )
40 opvtxfv ⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( I ↾ 𝑎 ) ∈ V ) → ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑎 ) ⟩ ) = 𝑉 )
41 31 40 sylan2 ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ) → ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑎 ) ⟩ ) = 𝑉 )
42 edgopval ⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( I ↾ 𝑎 ) ∈ V ) → ( Edg ‘ ⟨ 𝑉 , ( I ↾ 𝑎 ) ⟩ ) = ran ( I ↾ 𝑎 ) )
43 31 42 sylan2 ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ) → ( Edg ‘ ⟨ 𝑉 , ( I ↾ 𝑎 ) ⟩ ) = ran ( I ↾ 𝑎 ) )
44 rnresi ⊢ ran ( I ↾ 𝑎 ) = 𝑎
45 43 44 eqtrdi ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ) → ( Edg ‘ ⟨ 𝑉 , ( I ↾ 𝑎 ) ⟩ ) = 𝑎 )
46 41 45 jca ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ) → ( ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑎 ) ⟩ ) = 𝑉 ∧ ( Edg ‘ ⟨ 𝑉 , ( I ↾ 𝑎 ) ⟩ ) = 𝑎 ) )
47 46 ancoms ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) → ( ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑎 ) ⟩ ) = 𝑉 ∧ ( Edg ‘ ⟨ 𝑉 , ( I ↾ 𝑎 ) ⟩ ) = 𝑎 ) )
48 35 39 47 rspcedvd ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) → ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑉 ∧ ( Edg ‘ 𝑞 ) = 𝑎 ) )
49 9 48 jca ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) → ( 𝑉 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑉 ∧ ( Edg ‘ 𝑞 ) = 𝑎 ) ) )
50 2 eleq2i ⊢ ( ⟨ 𝑉 , 𝑎 ⟩ ∈ 𝐺 ↔ ⟨ 𝑉 , 𝑎 ⟩ ∈ { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) } )
51 30 anim1ci ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) → ( 𝑉 ∈ 𝑊 ∧ 𝑎 ∈ V ) )
52 eqeq1 ⊢ ( 𝑣 = 𝑉 → ( 𝑣 = 𝑉 ↔ 𝑉 = 𝑉 ) )
53 52 adantr ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝑎 ) → ( 𝑣 = 𝑉 ↔ 𝑉 = 𝑉 ) )
54 eqeq2 ⊢ ( 𝑣 = 𝑉 → ( ( Vtx ‘ 𝑞 ) = 𝑣 ↔ ( Vtx ‘ 𝑞 ) = 𝑉 ) )
55 eqeq2 ⊢ ( 𝑒 = 𝑎 → ( ( Edg ‘ 𝑞 ) = 𝑒 ↔ ( Edg ‘ 𝑞 ) = 𝑎 ) )
56 54 55 bi2anan9 ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝑎 ) → ( ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ↔ ( ( Vtx ‘ 𝑞 ) = 𝑉 ∧ ( Edg ‘ 𝑞 ) = 𝑎 ) ) )
57 56 rexbidv ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝑎 ) → ( ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ↔ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑉 ∧ ( Edg ‘ 𝑞 ) = 𝑎 ) ) )
58 53 57 anbi12d ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝑎 ) → ( ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) ↔ ( 𝑉 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑉 ∧ ( Edg ‘ 𝑞 ) = 𝑎 ) ) ) )
59 58 opelopabga ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑎 ∈ V ) → ( ⟨ 𝑉 , 𝑎 ⟩ ∈ { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) } ↔ ( 𝑉 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑉 ∧ ( Edg ‘ 𝑞 ) = 𝑎 ) ) ) )
60 51 59 syl ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) → ( ⟨ 𝑉 , 𝑎 ⟩ ∈ { ⟨ 𝑣 , 𝑒 ⟩ ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) } ↔ ( 𝑉 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑉 ∧ ( Edg ‘ 𝑞 ) = 𝑎 ) ) ) )
61 50 60 syl5bb ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) → ( ⟨ 𝑉 , 𝑎 ⟩ ∈ 𝐺 ↔ ( 𝑉 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑉 ∧ ( Edg ‘ 𝑞 ) = 𝑎 ) ) ) )
62 49 61 mpbird ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) → ⟨ 𝑉 , 𝑎 ⟩ ∈ 𝐺 )
63 fveq2 ⊢ ( 𝑏 = ⟨ 𝑉 , 𝑎 ⟩ → ( 2nd ‘ 𝑏 ) = ( 2nd ‘ ⟨ 𝑉 , 𝑎 ⟩ ) )
64 63 eqeq2d ⊢ ( 𝑏 = ⟨ 𝑉 , 𝑎 ⟩ → ( 𝑎 = ( 2nd ‘ 𝑏 ) ↔ 𝑎 = ( 2nd ‘ ⟨ 𝑉 , 𝑎 ⟩ ) ) )
65 64 adantl ⊢ ( ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) ∧ 𝑏 = ⟨ 𝑉 , 𝑎 ⟩ ) → ( 𝑎 = ( 2nd ‘ 𝑏 ) ↔ 𝑎 = ( 2nd ‘ ⟨ 𝑉 , 𝑎 ⟩ ) ) )
66 op2ndg ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑎 ∈ V ) → ( 2nd ‘ ⟨ 𝑉 , 𝑎 ⟩ ) = 𝑎 )
67 66 elvd ⊢ ( 𝑉 ∈ 𝑊 → ( 2nd ‘ ⟨ 𝑉 , 𝑎 ⟩ ) = 𝑎 )
68 67 adantl ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) → ( 2nd ‘ ⟨ 𝑉 , 𝑎 ⟩ ) = 𝑎 )
69 68 eqcomd ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) → 𝑎 = ( 2nd ‘ ⟨ 𝑉 , 𝑎 ⟩ ) )
70 62 65 69 rspcedvd ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑉 ∈ 𝑊 ) → ∃ 𝑏 ∈ 𝐺 𝑎 = ( 2nd ‘ 𝑏 ) )
71 70 ex ⊢ ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) → ( 𝑉 ∈ 𝑊 → ∃ 𝑏 ∈ 𝐺 𝑎 = ( 2nd ‘ 𝑏 ) ) )
72 8 71 sylbi ⊢ ( 𝑎 ∈ 𝑃 → ( 𝑉 ∈ 𝑊 → ∃ 𝑏 ∈ 𝐺 𝑎 = ( 2nd ‘ 𝑏 ) ) )
73 72 impcom ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑎 ∈ 𝑃 ) → ∃ 𝑏 ∈ 𝐺 𝑎 = ( 2nd ‘ 𝑏 ) )
74 1 2 3 uspgrsprfv ⊢ ( 𝑏 ∈ 𝐺 → ( 𝐹 ‘ 𝑏 ) = ( 2nd ‘ 𝑏 ) )
75 74 adantl ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝐺 ) → ( 𝐹 ‘ 𝑏 ) = ( 2nd ‘ 𝑏 ) )
76 75 eqeq2d ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝐺 ) → ( 𝑎 = ( 𝐹 ‘ 𝑏 ) ↔ 𝑎 = ( 2nd ‘ 𝑏 ) ) )
77 76 rexbidva ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑎 ∈ 𝑃 ) → ( ∃ 𝑏 ∈ 𝐺 𝑎 = ( 𝐹 ‘ 𝑏 ) ↔ ∃ 𝑏 ∈ 𝐺 𝑎 = ( 2nd ‘ 𝑏 ) ) )
78 73 77 mpbird ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑎 ∈ 𝑃 ) → ∃ 𝑏 ∈ 𝐺 𝑎 = ( 𝐹 ‘ 𝑏 ) )
79 78 ralrimiva ⊢ ( 𝑉 ∈ 𝑊 → ∀ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝐺 𝑎 = ( 𝐹 ‘ 𝑏 ) )
80 dffo3 ⊢ ( 𝐹 : 𝐺 –onto→ 𝑃 ↔ ( 𝐹 : 𝐺 ⟶ 𝑃 ∧ ∀ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝐺 𝑎 = ( 𝐹 ‘ 𝑏 ) ) )
81 5 79 80 sylanbrc ⊢ ( 𝑉 ∈ 𝑊 → 𝐹 : 𝐺 –onto→ 𝑃 )