Theorem funen1cnv

Description: If a function is equinumerous to ordinal 1, then its converse is also a function. (Contributed by BTernaryTau, 8-Oct-2023)

	Ref	Expression
Assertion	funen1cnv	⊢ ( ( Fun 𝐹 ∧ 𝐹 ≈ 1o ) → Fun ◡ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		en1	⊢ ( 𝐹 ≈ 1o ↔ ∃ 𝑝 𝐹 = { 𝑝 } )
2		funrel	⊢ ( Fun { 𝑝 } → Rel { 𝑝 } )
3		vsnid	⊢ 𝑝 ∈ { 𝑝 }
4		elrel	⊢ ( ( Rel { 𝑝 } ∧ 𝑝 ∈ { 𝑝 } ) → ∃ 𝑥 ∃ 𝑦 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ )
5	2 3 4	sylancl	⊢ ( Fun { 𝑝 } → ∃ 𝑥 ∃ 𝑦 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ )
6		sneq	⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → { 𝑝 } = { ⟨ 𝑥 , 𝑦 ⟩ } )
7	6	2eximi	⊢ ( ∃ 𝑥 ∃ 𝑦 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑥 ∃ 𝑦 { 𝑝 } = { ⟨ 𝑥 , 𝑦 ⟩ } )
8	5 7	syl	⊢ ( Fun { 𝑝 } → ∃ 𝑥 ∃ 𝑦 { 𝑝 } = { ⟨ 𝑥 , 𝑦 ⟩ } )
9		funcnvsn	⊢ Fun ◡ { ⟨ 𝑥 , 𝑦 ⟩ }
10	9	gen2	⊢ ∀ 𝑥 ∀ 𝑦 Fun ◡ { ⟨ 𝑥 , 𝑦 ⟩ }
11		19.29r2	⊢ ( ( ∃ 𝑥 ∃ 𝑦 { 𝑝 } = { ⟨ 𝑥 , 𝑦 ⟩ } ∧ ∀ 𝑥 ∀ 𝑦 Fun ◡ { ⟨ 𝑥 , 𝑦 ⟩ } ) → ∃ 𝑥 ∃ 𝑦 ( { 𝑝 } = { ⟨ 𝑥 , 𝑦 ⟩ } ∧ Fun ◡ { ⟨ 𝑥 , 𝑦 ⟩ } ) )
12		cnveq	⊢ ( { 𝑝 } = { ⟨ 𝑥 , 𝑦 ⟩ } → ◡ { 𝑝 } = ◡ { ⟨ 𝑥 , 𝑦 ⟩ } )
13	12	funeqd	⊢ ( { 𝑝 } = { ⟨ 𝑥 , 𝑦 ⟩ } → ( Fun ◡ { 𝑝 } ↔ Fun ◡ { ⟨ 𝑥 , 𝑦 ⟩ } ) )
14	13	biimpar	⊢ ( ( { 𝑝 } = { ⟨ 𝑥 , 𝑦 ⟩ } ∧ Fun ◡ { ⟨ 𝑥 , 𝑦 ⟩ } ) → Fun ◡ { 𝑝 } )
15	14	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( { 𝑝 } = { ⟨ 𝑥 , 𝑦 ⟩ } ∧ Fun ◡ { ⟨ 𝑥 , 𝑦 ⟩ } ) → Fun ◡ { 𝑝 } )
16	11 15	syl	⊢ ( ( ∃ 𝑥 ∃ 𝑦 { 𝑝 } = { ⟨ 𝑥 , 𝑦 ⟩ } ∧ ∀ 𝑥 ∀ 𝑦 Fun ◡ { ⟨ 𝑥 , 𝑦 ⟩ } ) → Fun ◡ { 𝑝 } )
17	8 10 16	sylancl	⊢ ( Fun { 𝑝 } → Fun ◡ { 𝑝 } )
18	17	ax-gen	⊢ ∀ 𝑝 ( Fun { 𝑝 } → Fun ◡ { 𝑝 } )
19		19.29r	⊢ ( ( ∃ 𝑝 𝐹 = { 𝑝 } ∧ ∀ 𝑝 ( Fun { 𝑝 } → Fun ◡ { 𝑝 } ) ) → ∃ 𝑝 ( 𝐹 = { 𝑝 } ∧ ( Fun { 𝑝 } → Fun ◡ { 𝑝 } ) ) )
20		funeq	⊢ ( 𝐹 = { 𝑝 } → ( Fun 𝐹 ↔ Fun { 𝑝 } ) )
21		cnveq	⊢ ( 𝐹 = { 𝑝 } → ◡ 𝐹 = ◡ { 𝑝 } )
22	21	funeqd	⊢ ( 𝐹 = { 𝑝 } → ( Fun ◡ 𝐹 ↔ Fun ◡ { 𝑝 } ) )
23	20 22	imbi12d	⊢ ( 𝐹 = { 𝑝 } → ( ( Fun 𝐹 → Fun ◡ 𝐹 ) ↔ ( Fun { 𝑝 } → Fun ◡ { 𝑝 } ) ) )
24	23	biimpar	⊢ ( ( 𝐹 = { 𝑝 } ∧ ( Fun { 𝑝 } → Fun ◡ { 𝑝 } ) ) → ( Fun 𝐹 → Fun ◡ 𝐹 ) )
25	24	exlimiv	⊢ ( ∃ 𝑝 ( 𝐹 = { 𝑝 } ∧ ( Fun { 𝑝 } → Fun ◡ { 𝑝 } ) ) → ( Fun 𝐹 → Fun ◡ 𝐹 ) )
26	19 25	syl	⊢ ( ( ∃ 𝑝 𝐹 = { 𝑝 } ∧ ∀ 𝑝 ( Fun { 𝑝 } → Fun ◡ { 𝑝 } ) ) → ( Fun 𝐹 → Fun ◡ 𝐹 ) )
27	18 26	mpan2	⊢ ( ∃ 𝑝 𝐹 = { 𝑝 } → ( Fun 𝐹 → Fun ◡ 𝐹 ) )
28	1 27	sylbi	⊢ ( 𝐹 ≈ 1o → ( Fun 𝐹 → Fun ◡ 𝐹 ) )
29	28	impcom	⊢ ( ( Fun 𝐹 ∧ 𝐹 ≈ 1o ) → Fun ◡ 𝐹 )