Theorem isplig

Description: The predicate "is a planar incidence geometry" for sets. (Contributed by FL, 2-Aug-2009)

	Ref	Expression
Hypothesis	isplig.1	⊢ 𝑃 = ∪ 𝐺
Assertion	isplig	⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ Plig ↔ ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ∧ ∀ 𝑙 ∈ 𝐺 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∀ 𝑙 ∈ 𝐺 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isplig.1	⊢ 𝑃 = ∪ 𝐺
2		unieq	⊢ ( 𝑥 = 𝐺 → ∪ 𝑥 = ∪ 𝐺 )
3	2 1	eqtr4di	⊢ ( 𝑥 = 𝐺 → ∪ 𝑥 = 𝑃 )
4		reueq1	⊢ ( 𝑥 = 𝐺 → ( ∃! 𝑙 ∈ 𝑥 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ↔ ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) )
5	4	imbi2d	⊢ ( 𝑥 = 𝐺 → ( ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝑥 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ↔ ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ) )
6	3 5	raleqbidv	⊢ ( 𝑥 = 𝐺 → ( ∀ 𝑏 ∈ ∪ 𝑥 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝑥 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ↔ ∀ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ) )
7	3 6	raleqbidv	⊢ ( 𝑥 = 𝐺 → ( ∀ 𝑎 ∈ ∪ 𝑥 ∀ 𝑏 ∈ ∪ 𝑥 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝑥 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ↔ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ) )
8	3	rexeqdv	⊢ ( 𝑥 = 𝐺 → ( ∃ 𝑏 ∈ ∪ 𝑥 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ↔ ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) )
9	3 8	rexeqbidv	⊢ ( 𝑥 = 𝐺 → ( ∃ 𝑎 ∈ ∪ 𝑥 ∃ 𝑏 ∈ ∪ 𝑥 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ↔ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) )
10	9	raleqbi1dv	⊢ ( 𝑥 = 𝐺 → ( ∀ 𝑙 ∈ 𝑥 ∃ 𝑎 ∈ ∪ 𝑥 ∃ 𝑏 ∈ ∪ 𝑥 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ↔ ∀ 𝑙 ∈ 𝐺 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) )
11		raleq	⊢ ( 𝑥 = 𝐺 → ( ∀ 𝑙 ∈ 𝑥 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ↔ ∀ 𝑙 ∈ 𝐺 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ) )
12	3 11	rexeqbidv	⊢ ( 𝑥 = 𝐺 → ( ∃ 𝑐 ∈ ∪ 𝑥 ∀ 𝑙 ∈ 𝑥 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ↔ ∃ 𝑐 ∈ 𝑃 ∀ 𝑙 ∈ 𝐺 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ) )
13	3 12	rexeqbidv	⊢ ( 𝑥 = 𝐺 → ( ∃ 𝑏 ∈ ∪ 𝑥 ∃ 𝑐 ∈ ∪ 𝑥 ∀ 𝑙 ∈ 𝑥 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ↔ ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∀ 𝑙 ∈ 𝐺 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ) )
14	3 13	rexeqbidv	⊢ ( 𝑥 = 𝐺 → ( ∃ 𝑎 ∈ ∪ 𝑥 ∃ 𝑏 ∈ ∪ 𝑥 ∃ 𝑐 ∈ ∪ 𝑥 ∀ 𝑙 ∈ 𝑥 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ↔ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∀ 𝑙 ∈ 𝐺 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ) )
15	7 10 14	3anbi123d	⊢ ( 𝑥 = 𝐺 → ( ( ∀ 𝑎 ∈ ∪ 𝑥 ∀ 𝑏 ∈ ∪ 𝑥 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝑥 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ∧ ∀ 𝑙 ∈ 𝑥 ∃ 𝑎 ∈ ∪ 𝑥 ∃ 𝑏 ∈ ∪ 𝑥 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ∧ ∃ 𝑎 ∈ ∪ 𝑥 ∃ 𝑏 ∈ ∪ 𝑥 ∃ 𝑐 ∈ ∪ 𝑥 ∀ 𝑙 ∈ 𝑥 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ) ↔ ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ∧ ∀ 𝑙 ∈ 𝐺 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∀ 𝑙 ∈ 𝐺 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ) ) )
16		df-plig	⊢ Plig = { 𝑥 ∣ ( ∀ 𝑎 ∈ ∪ 𝑥 ∀ 𝑏 ∈ ∪ 𝑥 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝑥 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ∧ ∀ 𝑙 ∈ 𝑥 ∃ 𝑎 ∈ ∪ 𝑥 ∃ 𝑏 ∈ ∪ 𝑥 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ∧ ∃ 𝑎 ∈ ∪ 𝑥 ∃ 𝑏 ∈ ∪ 𝑥 ∃ 𝑐 ∈ ∪ 𝑥 ∀ 𝑙 ∈ 𝑥 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ) }
17	15 16	elab2g	⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ Plig ↔ ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝐺 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ∧ ∀ 𝑙 ∈ 𝐺 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∀ 𝑙 ∈ 𝐺 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ) ) )