Metamath Proof Explorer


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 ↔ ( ∀ 𝑎𝑃𝑏𝑃 ( 𝑎𝑏 → ∃! 𝑙𝐺 ( 𝑎𝑙𝑏𝑙 ) ) ∧ ∀ 𝑙𝐺𝑎𝑃𝑏𝑃 ( 𝑎𝑏𝑎𝑙𝑏𝑙 ) ∧ ∃ 𝑎𝑃𝑏𝑃𝑐𝑃𝑙𝐺 ¬ ( 𝑎𝑙𝑏𝑙𝑐𝑙 ) ) ) )