Step |
Hyp |
Ref |
Expression |
1 |
|
tglng.p |
⊢ 𝑃 = ( Base ‘ 𝐺 ) |
2 |
|
tglng.l |
⊢ 𝐿 = ( LineG ‘ 𝐺 ) |
3 |
|
tglng.i |
⊢ 𝐼 = ( Itv ‘ 𝐺 ) |
4 |
1
|
fvexi |
⊢ 𝑃 ∈ V |
5 |
4
|
rabex |
⊢ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ∈ V |
6 |
5
|
rgen2w |
⊢ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ∈ V |
7 |
|
eqid |
⊢ ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) |
8 |
7
|
fmpox |
⊢ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ∈ V ↔ ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) : ∪ 𝑥 ∈ 𝑃 ( { 𝑥 } × ( 𝑃 ∖ { 𝑥 } ) ) ⟶ V ) |
9 |
6 8
|
mpbi |
⊢ ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) : ∪ 𝑥 ∈ 𝑃 ( { 𝑥 } × ( 𝑃 ∖ { 𝑥 } ) ) ⟶ V |
10 |
|
ffn |
⊢ ( ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) : ∪ 𝑥 ∈ 𝑃 ( { 𝑥 } × ( 𝑃 ∖ { 𝑥 } ) ) ⟶ V → ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) Fn ∪ 𝑥 ∈ 𝑃 ( { 𝑥 } × ( 𝑃 ∖ { 𝑥 } ) ) ) |
11 |
9 10
|
ax-mp |
⊢ ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) Fn ∪ 𝑥 ∈ 𝑃 ( { 𝑥 } × ( 𝑃 ∖ { 𝑥 } ) ) |
12 |
|
xpdifid |
⊢ ∪ 𝑥 ∈ 𝑃 ( { 𝑥 } × ( 𝑃 ∖ { 𝑥 } ) ) = ( ( 𝑃 × 𝑃 ) ∖ I ) |
13 |
12
|
fneq2i |
⊢ ( ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) Fn ∪ 𝑥 ∈ 𝑃 ( { 𝑥 } × ( 𝑃 ∖ { 𝑥 } ) ) ↔ ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) Fn ( ( 𝑃 × 𝑃 ) ∖ I ) ) |
14 |
11 13
|
mpbi |
⊢ ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) Fn ( ( 𝑃 × 𝑃 ) ∖ I ) |
15 |
1 2 3
|
tglng |
⊢ ( 𝐺 ∈ TarskiG → 𝐿 = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ) |
16 |
15
|
fneq1d |
⊢ ( 𝐺 ∈ TarskiG → ( 𝐿 Fn ( ( 𝑃 × 𝑃 ) ∖ I ) ↔ ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) Fn ( ( 𝑃 × 𝑃 ) ∖ I ) ) ) |
17 |
14 16
|
mpbiri |
⊢ ( 𝐺 ∈ TarskiG → 𝐿 Fn ( ( 𝑃 × 𝑃 ) ∖ I ) ) |