Theorem isline

Description: The predicate "is a line". (Contributed by NM, 19-Sep-2011)

	Ref	Expression
Hypotheses	isline.l	⊢ ≤ = ( le ‘ 𝐾 )
	isline.j	⊢ ∨ = ( join ‘ 𝐾 )
	isline.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	isline.n	⊢ 𝑁 = ( Lines ‘ 𝐾 )
Assertion	isline	⊢ ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝑁 ↔ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		isline.l	⊢ ≤ = ( le ‘ 𝐾 )
2		isline.j	⊢ ∨ = ( join ‘ 𝐾 )
3		isline.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		isline.n	⊢ 𝑁 = ( Lines ‘ 𝐾 )
5	1 2 3 4	lineset	⊢ ( 𝐾 ∈ 𝐷 → 𝑁 = { 𝑥 ∣ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑥 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) } )
6	5	eleq2d	⊢ ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝑁 ↔ 𝑋 ∈ { 𝑥 ∣ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑥 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) } ) )
7	3	fvexi	⊢ 𝐴 ∈ V
8	7	rabex	⊢ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ∈ V
9		eleq1	⊢ ( 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } → ( 𝑋 ∈ V ↔ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ∈ V ) )
10	8 9	mpbiri	⊢ ( 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } → 𝑋 ∈ V )
11	10	adantl	⊢ ( ( 𝑞 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) → 𝑋 ∈ V )
12	11	a1i	⊢ ( ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) → ( ( 𝑞 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) → 𝑋 ∈ V ) )
13	12	rexlimivv	⊢ ( ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) → 𝑋 ∈ V )
14		eqeq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ↔ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) )
15	14	anbi2d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑞 ≠ 𝑟 ∧ 𝑥 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ↔ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )
16	15	2rexbidv	⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑥 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ↔ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )
17	13 16	elab3	⊢ ( 𝑋 ∈ { 𝑥 ∣ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑥 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) } ↔ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) )
18	6 17	bitrdi	⊢ ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝑁 ↔ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )