Theorem perpln2

Description: Derive a line from perpendicularity. (Contributed by Thierry Arnoux, 27-Nov-2019)

	Ref	Expression
Hypotheses	perpln.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	perpln.1	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	perpln.2	⊢ ( 𝜑 → 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 )
Assertion	perpln2	⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )

Proof

Step	Hyp	Ref	Expression
1		perpln.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
2		perpln.1	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
3		perpln.2	⊢ ( 𝜑 → 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 )
4		df-perpg	⊢ ⟂G = ( 𝑔 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝑔 ) ) } )
5		simpr	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
6	5	fveq2d	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( LineG ‘ 𝑔 ) = ( LineG ‘ 𝐺 ) )
7	6 1	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( LineG ‘ 𝑔 ) = 𝐿 )
8	7	rneqd	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ran ( LineG ‘ 𝑔 ) = ran 𝐿 )
9	8	eleq2d	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ↔ 𝑎 ∈ ran 𝐿 ) )
10	8	eleq2d	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ↔ 𝑏 ∈ ran 𝐿 ) )
11	9 10	anbi12d	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ) ↔ ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ) )
12	5	fveq2d	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( ∟G ‘ 𝑔 ) = ( ∟G ‘ 𝐺 ) )
13	12	eleq2d	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝑔 ) ↔ ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
14	13	ralbidv	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝑔 ) ↔ ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
15	14	rexralbidv	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝑔 ) ↔ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
16	11 15	anbi12d	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( ( ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝑔 ) ) ↔ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ) )
17	16	opabbidv	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝑔 ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) } )
18	2	elexd	⊢ ( 𝜑 → 𝐺 ∈ V )
19	1	fvexi	⊢ 𝐿 ∈ V
20		rnexg	⊢ ( 𝐿 ∈ V → ran 𝐿 ∈ V )
21	19 20	mp1i	⊢ ( 𝜑 → ran 𝐿 ∈ V )
22	21 21	xpexd	⊢ ( 𝜑 → ( ran 𝐿 × ran 𝐿 ) ∈ V )
23		opabssxp	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) } ⊆ ( ran 𝐿 × ran 𝐿 )
24	23	a1i	⊢ ( 𝜑 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) } ⊆ ( ran 𝐿 × ran 𝐿 ) )
25	22 24	ssexd	⊢ ( 𝜑 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) } ∈ V )
26	4 17 18 25	fvmptd2	⊢ ( 𝜑 → ( ⟂G ‘ 𝐺 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) } )
27	26	rneqd	⊢ ( 𝜑 → ran ( ⟂G ‘ 𝐺 ) = ran { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) } )
28	23	rnssi	⊢ ran { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) } ⊆ ran ( ran 𝐿 × ran 𝐿 )
29	27 28	eqsstrdi	⊢ ( 𝜑 → ran ( ⟂G ‘ 𝐺 ) ⊆ ran ( ran 𝐿 × ran 𝐿 ) )
30		rnxpss	⊢ ran ( ran 𝐿 × ran 𝐿 ) ⊆ ran 𝐿
31	29 30	sstrdi	⊢ ( 𝜑 → ran ( ⟂G ‘ 𝐺 ) ⊆ ran 𝐿 )
32		relopabv	⊢ Rel { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) }
33	26	releqd	⊢ ( 𝜑 → ( Rel ( ⟂G ‘ 𝐺 ) ↔ Rel { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) } ) )
34	32 33	mpbiri	⊢ ( 𝜑 → Rel ( ⟂G ‘ 𝐺 ) )
35		brrelex12	⊢ ( ( Rel ( ⟂G ‘ 𝐺 ) ∧ 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
36	34 3 35	syl2anc	⊢ ( 𝜑 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
37	36	simpld	⊢ ( 𝜑 → 𝐴 ∈ V )
38	36	simprd	⊢ ( 𝜑 → 𝐵 ∈ V )
39		brelrng	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ) → 𝐵 ∈ ran ( ⟂G ‘ 𝐺 ) )
40	37 38 3 39	syl3anc	⊢ ( 𝜑 → 𝐵 ∈ ran ( ⟂G ‘ 𝐺 ) )
41	31 40	sseldd	⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )