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