Theorem inlinecirc02preu

Description: Intersection of a line with a circle: A line passing through a point within a circle around the origin intersects the circle at exactly two different points, expressed with restricted uniqueness (and without the definition of proper pairs). (Contributed by AV, 16-May-2023)

	Ref	Expression
Hypotheses	inlinecirc02p.i	⊢ 𝐼 = { 1 , 2 }
	inlinecirc02p.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
	inlinecirc02p.p	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
	inlinecirc02p.s	⊢ 𝑆 = ( Sphere ‘ 𝐸 )
	inlinecirc02p.0	⊢ 0 = ( 𝐼 × { 0 } )
	inlinecirc02p.l	⊢ 𝐿 = ( LineM ‘ 𝐸 )
	inlinecirc02p.d	⊢ 𝐷 = ( dist ‘ 𝐸 )
Assertion	inlinecirc02preu	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ∃! 𝑝 ∈ 𝒫 𝑃 ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝑝 = ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		inlinecirc02p.i	⊢ 𝐼 = { 1 , 2 }
2		inlinecirc02p.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3		inlinecirc02p.p	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
4		inlinecirc02p.s	⊢ 𝑆 = ( Sphere ‘ 𝐸 )
5		inlinecirc02p.0	⊢ 0 = ( 𝐼 × { 0 } )
6		inlinecirc02p.l	⊢ 𝐿 = ( LineM ‘ 𝐸 )
7		inlinecirc02p.d	⊢ 𝐷 = ( dist ‘ 𝐸 )
8	1 2 3 4 5 6 7	inlinecirc02p	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) ∈ ( Pairsproper ‘ 𝑃 ) )
9		reueq	⊢ ( ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) ∈ ( Pairsproper ‘ 𝑃 ) ↔ ∃! 𝑝 ∈ ( Pairsproper ‘ 𝑃 ) 𝑝 = ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) )
10	8 9	sylib	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ∃! 𝑝 ∈ ( Pairsproper ‘ 𝑃 ) 𝑝 = ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) )
11	3	ovexi	⊢ 𝑃 ∈ V
12		prprreueq	⊢ ( 𝑃 ∈ V → ( ∃! 𝑝 ∈ ( Pairsproper ‘ 𝑃 ) 𝑝 = ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) ↔ ∃! 𝑝 ∈ 𝒫 𝑃 ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝑝 = ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) ) ) )
13	11 12	mp1i	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ∃! 𝑝 ∈ ( Pairsproper ‘ 𝑃 ) 𝑝 = ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) ↔ ∃! 𝑝 ∈ 𝒫 𝑃 ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝑝 = ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) ) ) )
14	10 13	mpbid	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ∃! 𝑝 ∈ 𝒫 𝑃 ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝑝 = ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) ) )