Metamath Proof Explorer

Theorem ellines

Description: Membership in the set of all lines. (Contributed by Scott Fenton, 28-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion ellines ( 𝐴 ∈ LinesEE ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ 𝐴 = ( 𝑝 Line 𝑞 ) ) )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐴 ∈ LinesEE → 𝐴 ∈ V )
2 ovex ⊢ ( 𝑝 Line 𝑞 ) ∈ V
3 eleq1 ⊢ ( 𝐴 = ( 𝑝 Line 𝑞 ) → ( 𝐴 ∈ V ↔ ( 𝑝 Line 𝑞 ) ∈ V ) )
4 2 3 mpbiri ⊢ ( 𝐴 = ( 𝑝 Line 𝑞 ) → 𝐴 ∈ V )
5 4 adantl ⊢ ( ( 𝑝 ≠ 𝑞 ∧ 𝐴 = ( 𝑝 Line 𝑞 ) ) → 𝐴 ∈ V )
6 5 rexlimivw ⊢ ( ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ 𝐴 = ( 𝑝 Line 𝑞 ) ) → 𝐴 ∈ V )
7 6 a1i ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) → ( ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ 𝐴 = ( 𝑝 Line 𝑞 ) ) → 𝐴 ∈ V ) )
8 7 rexlimivv ⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ 𝐴 = ( 𝑝 Line 𝑞 ) ) → 𝐴 ∈ V )
9 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ LinesEE ↔ 𝐴 ∈ LinesEE ) )
10 eqeq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 = ( 𝑝 Line 𝑞 ) ↔ 𝐴 = ( 𝑝 Line 𝑞 ) ) )
11 10 anbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ↔ ( 𝑝 ≠ 𝑞 ∧ 𝐴 = ( 𝑝 Line 𝑞 ) ) ) )
12 11 rexbidv ⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ↔ ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ 𝐴 = ( 𝑝 Line 𝑞 ) ) ) )
13 12 2rexbidv ⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ 𝐴 = ( 𝑝 Line 𝑞 ) ) ) )
14 df-lines2 ⊢ LinesEE = ran Line
15 df-line2 ⊢ Line = { ⟨ ⟨ 𝑝 , 𝑞 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ∧ 𝑥 = [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear ) }
16 15 rneqi ⊢ ran Line = ran { ⟨ ⟨ 𝑝 , 𝑞 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ∧ 𝑥 = [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear ) }
17 rnoprab ⊢ ran { ⟨ ⟨ 𝑝 , 𝑞 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ∧ 𝑥 = [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear ) } = { 𝑥 ∣ ∃ 𝑝 ∃ 𝑞 ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ∧ 𝑥 = [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear ) }
18 14 16 17 3eqtri ⊢ LinesEE = { 𝑥 ∣ ∃ 𝑝 ∃ 𝑞 ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ∧ 𝑥 = [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear ) }
19 18 eleq2i ⊢ ( 𝑥 ∈ LinesEE ↔ 𝑥 ∈ { 𝑥 ∣ ∃ 𝑝 ∃ 𝑞 ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ∧ 𝑥 = [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear ) } )
20 abid ⊢ ( 𝑥 ∈ { 𝑥 ∣ ∃ 𝑝 ∃ 𝑞 ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ∧ 𝑥 = [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear ) } ↔ ∃ 𝑝 ∃ 𝑞 ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ∧ 𝑥 = [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear ) )
21 df-rex ⊢ ( ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ∧ 𝑥 = [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear ) ↔ ∃ 𝑛 ( 𝑛 ∈ ℕ ∧ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ∧ 𝑥 = [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear ) ) )
22 21 2exbii ⊢ ( ∃ 𝑝 ∃ 𝑞 ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ∧ 𝑥 = [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear ) ↔ ∃ 𝑝 ∃ 𝑞 ∃ 𝑛 ( 𝑛 ∈ ℕ ∧ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ∧ 𝑥 = [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear ) ) )
23 exrot3 ⊢ ( ∃ 𝑛 ∃ 𝑝 ∃ 𝑞 ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ) ) ↔ ∃ 𝑝 ∃ 𝑞 ∃ 𝑛 ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ) ) )
24 r2ex ⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ↔ ∃ 𝑛 ∃ 𝑝 ( ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ) )
25 r19.42v ⊢ ( ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ) ↔ ( ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ) )
26 df-rex ⊢ ( ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ) ↔ ∃ 𝑞 ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ) ) )
27 25 26 bitr3i ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ) ↔ ∃ 𝑞 ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ) ) )
28 27 2exbii ⊢ ( ∃ 𝑛 ∃ 𝑝 ( ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ) ↔ ∃ 𝑛 ∃ 𝑝 ∃ 𝑞 ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ) ) )
29 24 28 bitri ⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ↔ ∃ 𝑛 ∃ 𝑝 ∃ 𝑞 ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ) ) )
30 anass ⊢ ( ( ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ) ↔ ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ) ) )
31 anass ⊢ ( ( ( ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ∧ 𝑝 ≠ 𝑞 ) ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ↔ ( ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ) )
32 simplrl ⊢ ( ( ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝑛 ∈ ℕ )
33 simplrr ⊢ ( ( ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) )
34 simpll ⊢ ( ( ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) )
35 simpr ⊢ ( ( ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → 𝑝 ≠ 𝑞 )
36 33 34 35 3jca ⊢ ( ( ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) )
37 32 36 jca ⊢ ( ( ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ∧ 𝑝 ≠ 𝑞 ) → ( 𝑛 ∈ ℕ ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ) )
38 simpr2 ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ) → 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) )
39 simpl ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ) → 𝑛 ∈ ℕ )
40 simpr1 ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ) → 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) )
41 38 39 40 jca32 ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ) → ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ) )
42 simpr3 ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ) → 𝑝 ≠ 𝑞 )
43 41 42 jca ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ) → ( ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ∧ 𝑝 ≠ 𝑞 ) )
44 37 43 impbii ⊢ ( ( ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ∧ 𝑝 ≠ 𝑞 ) ↔ ( 𝑛 ∈ ℕ ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ) )
45 44 anbi1i ⊢ ( ( ( ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ∧ 𝑝 ≠ 𝑞 ) ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ↔ ( ( 𝑛 ∈ ℕ ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ) ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) )
46 31 45 bitr3i ⊢ ( ( ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ) ↔ ( ( 𝑛 ∈ ℕ ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ) ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) )
47 30 46 bitr3i ⊢ ( ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ) ) ↔ ( ( 𝑛 ∈ ℕ ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ) ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) )
48 fvline ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ) → ( 𝑝 Line 𝑞 ) = { 𝑥 ∣ 𝑥 Colinear ⟨ 𝑝 , 𝑞 ⟩ } )
49 opex ⊢ ⟨ 𝑝 , 𝑞 ⟩ ∈ V
50 dfec2 ⊢ ( ⟨ 𝑝 , 𝑞 ⟩ ∈ V → [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear = { 𝑥 ∣ ⟨ 𝑝 , 𝑞 ⟩ ◡ Colinear 𝑥 } )
51 49 50 ax-mp ⊢ [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear = { 𝑥 ∣ ⟨ 𝑝 , 𝑞 ⟩ ◡ Colinear 𝑥 }
52 vex ⊢ 𝑥 ∈ V
53 49 52 brcnv ⊢ ( ⟨ 𝑝 , 𝑞 ⟩ ◡ Colinear 𝑥 ↔ 𝑥 Colinear ⟨ 𝑝 , 𝑞 ⟩ )
54 53 abbii ⊢ { 𝑥 ∣ ⟨ 𝑝 , 𝑞 ⟩ ◡ Colinear 𝑥 } = { 𝑥 ∣ 𝑥 Colinear ⟨ 𝑝 , 𝑞 ⟩ }
55 51 54 eqtri ⊢ [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear = { 𝑥 ∣ 𝑥 Colinear ⟨ 𝑝 , 𝑞 ⟩ }
56 48 55 eqtr4di ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ) → ( 𝑝 Line 𝑞 ) = [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear )
57 56 eqeq2d ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ) → ( 𝑥 = ( 𝑝 Line 𝑞 ) ↔ 𝑥 = [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear ) )
58 57 pm5.32i ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ) ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ↔ ( ( 𝑛 ∈ ℕ ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ) ∧ 𝑥 = [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear ) )
59 anass ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ) ∧ 𝑥 = [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear ) ↔ ( 𝑛 ∈ ℕ ∧ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ∧ 𝑥 = [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear ) ) )
60 47 58 59 3bitrri ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ∧ 𝑥 = [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear ) ) ↔ ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ) ) )
61 60 3exbii ⊢ ( ∃ 𝑝 ∃ 𝑞 ∃ 𝑛 ( 𝑛 ∈ ℕ ∧ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ∧ 𝑥 = [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear ) ) ↔ ∃ 𝑝 ∃ 𝑞 ∃ 𝑛 ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) ) ) )
62 23 29 61 3bitr4ri ⊢ ( ∃ 𝑝 ∃ 𝑞 ∃ 𝑛 ( 𝑛 ∈ ℕ ∧ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ∧ 𝑥 = [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear ) ) ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) )
63 22 62 bitri ⊢ ( ∃ 𝑝 ∃ 𝑞 ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ∧ 𝑥 = [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear ) ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) )
64 20 63 bitri ⊢ ( 𝑥 ∈ { 𝑥 ∣ ∃ 𝑝 ∃ 𝑞 ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑞 ) ∧ 𝑥 = [ ⟨ 𝑝 , 𝑞 ⟩ ] ◡ Colinear ) } ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) )
65 19 64 bitri ⊢ ( 𝑥 ∈ LinesEE ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ 𝑥 = ( 𝑝 Line 𝑞 ) ) )
66 9 13 65 vtoclbg ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ LinesEE ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ 𝐴 = ( 𝑝 Line 𝑞 ) ) ) )
67 1 8 66 pm5.21nii ⊢ ( 𝐴 ∈ LinesEE ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 ≠ 𝑞 ∧ 𝐴 = ( 𝑝 Line 𝑞 ) ) )