Theorem perpln1

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	perpln1	⊢ ( 𝜑 → 𝐴 ∈ 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		anass	⊢ ( ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ↔ ( 𝑎 ∈ ran 𝐿 ∧ ( 𝑏 ∈ ran 𝐿 ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ) )
28	27	opabbii	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ran 𝐿 ∧ ( 𝑏 ∈ ran 𝐿 ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ) }
29	26 28	eqtrdi	⊢ ( 𝜑 → ( ⟂G ‘ 𝐺 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ran 𝐿 ∧ ( 𝑏 ∈ ran 𝐿 ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ) } )
30	29	dmeqd	⊢ ( 𝜑 → dom ( ⟂G ‘ 𝐺 ) = dom { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ran 𝐿 ∧ ( 𝑏 ∈ ran 𝐿 ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ) } )
31		dmopabss	⊢ dom { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ ran 𝐿 ∧ ( 𝑏 ∈ ran 𝐿 ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ) } ⊆ ran 𝐿
32	30 31	eqsstrdi	⊢ ( 𝜑 → dom ( ⟂G ‘ 𝐺 ) ⊆ ran 𝐿 )
33		relopabv	⊢ Rel { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) }
34	26	releqd	⊢ ( 𝜑 → ( Rel ( ⟂G ‘ 𝐺 ) ↔ Rel { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) } ) )
35	33 34	mpbiri	⊢ ( 𝜑 → Rel ( ⟂G ‘ 𝐺 ) )
36		brrelex12	⊢ ( ( Rel ( ⟂G ‘ 𝐺 ) ∧ 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
37	35 3 36	syl2anc	⊢ ( 𝜑 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
38	37	simpld	⊢ ( 𝜑 → 𝐴 ∈ V )
39	37	simprd	⊢ ( 𝜑 → 𝐵 ∈ V )
40		breldmg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ) → 𝐴 ∈ dom ( ⟂G ‘ 𝐺 ) )
41	38 39 3 40	syl3anc	⊢ ( 𝜑 → 𝐴 ∈ dom ( ⟂G ‘ 𝐺 ) )
42	32 41	sseldd	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )