Metamath Proof Explorer

Theorem istrkg2ld

Description: Property of fulfilling the lower dimension 2 axiom. (Contributed by Thierry Arnoux, 20-Nov-2019)

Ref Expression
Hypotheses istrkg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
istrkg.d ⊢ − = ( dist ‘ 𝐺 )
istrkg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
Assertion istrkg2ld ( 𝐺 ∈ 𝑉 → ( 𝐺 DimTarskiG≥ 2 ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) )

Proof

Step Hyp Ref Expression
1 istrkg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 istrkg.d ⊢ − = ( dist ‘ 𝐺 )
3 istrkg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 2z ⊢ 2 ∈ ℤ
5 uzid ⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) )
6 4 5 ax-mp ⊢ 2 ∈ ( ℤ≥ ‘ 2 )
7 1 2 3 istrkgld ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 2 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐺 DimTarskiG≥ 2 ↔ ∃ 𝑓 ( 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
8 6 7 mpan2 ⊢ ( 𝐺 ∈ 𝑉 → ( 𝐺 DimTarskiG≥ 2 ↔ ∃ 𝑓 ( 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
9 r19.41v ⊢ ( ∃ 𝑥 ∈ 𝑃 ( ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ∧ 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ) ↔ ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ∧ 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ) )
10 ancom ⊢ ( ( ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ∧ 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ) ↔ ( 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ∧ ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
11 10 rexbii ⊢ ( ∃ 𝑥 ∈ 𝑃 ( ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ∧ 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ) ↔ ∃ 𝑥 ∈ 𝑃 ( 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ∧ ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
12 ancom ⊢ ( ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ∧ 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ) ↔ ( 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
13 9 11 12 3bitr3ri ⊢ ( ( 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ∃ 𝑥 ∈ 𝑃 ( 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ∧ ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
14 13 exbii ⊢ ( ∃ 𝑓 ( 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ∃ 𝑓 ∃ 𝑥 ∈ 𝑃 ( 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ∧ ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
15 rexcom4 ⊢ ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑓 ( 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ∧ ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ∃ 𝑓 ∃ 𝑥 ∈ 𝑃 ( 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ∧ ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
16 simpr ⊢ ( ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) → ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) )
17 16 reximi ⊢ ( ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) → ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) )
18 17 reximi ⊢ ( ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) → ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) )
19 18 adantl ⊢ ( ( 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ∧ ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) → ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) )
20 19 exlimiv ⊢ ( ∃ 𝑓 ( 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ∧ ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) → ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) )
21 20 adantl ⊢ ( ( 𝑥 ∈ 𝑃 ∧ ∃ 𝑓 ( 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ∧ ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) → ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) )
22 1ex ⊢ 1 ∈ V
23 vex ⊢ 𝑥 ∈ V
24 22 23 f1osn ⊢ { ⟨ 1 , 𝑥 ⟩ } : { 1 } –1-1-onto→ { 𝑥 }
25 f1of1 ⊢ ( { ⟨ 1 , 𝑥 ⟩ } : { 1 } –1-1-onto→ { 𝑥 } → { ⟨ 1 , 𝑥 ⟩ } : { 1 } –1-1→ { 𝑥 } )
26 24 25 mp1i ⊢ ( 𝑥 ∈ 𝑃 → { ⟨ 1 , 𝑥 ⟩ } : { 1 } –1-1→ { 𝑥 } )
27 snssi ⊢ ( 𝑥 ∈ 𝑃 → { 𝑥 } ⊆ 𝑃 )
28 f1ss ⊢ ( ( { ⟨ 1 , 𝑥 ⟩ } : { 1 } –1-1→ { 𝑥 } ∧ { 𝑥 } ⊆ 𝑃 ) → { ⟨ 1 , 𝑥 ⟩ } : { 1 } –1-1→ 𝑃 )
29 26 27 28 syl2anc ⊢ ( 𝑥 ∈ 𝑃 → { ⟨ 1 , 𝑥 ⟩ } : { 1 } –1-1→ 𝑃 )
30 fzo12sn ⊢ ( 1 ..^ 2 ) = { 1 }
31 30 mpteq1i ⊢ ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) = ( 𝑗 ∈ { 1 } ↦ 𝑥 )
32 fmptsn ⊢ ( ( 1 ∈ V ∧ 𝑥 ∈ V ) → { ⟨ 1 , 𝑥 ⟩ } = ( 𝑗 ∈ { 1 } ↦ 𝑥 ) )
33 22 23 32 mp2an ⊢ { ⟨ 1 , 𝑥 ⟩ } = ( 𝑗 ∈ { 1 } ↦ 𝑥 )
34 31 33 eqtr4i ⊢ ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) = { ⟨ 1 , 𝑥 ⟩ }
35 34 a1i ⊢ ( ⊤ → ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) = { ⟨ 1 , 𝑥 ⟩ } )
36 30 a1i ⊢ ( ⊤ → ( 1 ..^ 2 ) = { 1 } )
37 eqidd ⊢ ( ⊤ → 𝑃 = 𝑃 )
38 35 36 37 f1eq123d ⊢ ( ⊤ → ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) : ( 1 ..^ 2 ) –1-1→ 𝑃 ↔ { ⟨ 1 , 𝑥 ⟩ } : { 1 } –1-1→ 𝑃 ) )
39 38 mptru ⊢ ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) : ( 1 ..^ 2 ) –1-1→ 𝑃 ↔ { ⟨ 1 , 𝑥 ⟩ } : { 1 } –1-1→ 𝑃 )
40 29 39 sylibr ⊢ ( 𝑥 ∈ 𝑃 → ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) : ( 1 ..^ 2 ) –1-1→ 𝑃 )
41 ral0 ⊢ ∀ 𝑗 ∈ ∅ ( ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑥 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑥 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑦 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑦 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑧 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑧 ) )
42 fzo0 ⊢ ( 2 ..^ 2 ) = ∅
43 42 raleqi ⊢ ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑥 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑥 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑦 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑦 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑧 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑧 ) ) ↔ ∀ 𝑗 ∈ ∅ ( ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑥 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑥 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑦 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑦 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑧 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑧 ) ) )
44 41 43 mpbir ⊢ ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑥 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑥 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑦 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑦 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑧 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑧 ) )
45 44 jctl ⊢ ( ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) → ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑥 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑥 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑦 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑦 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑧 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) )
46 45 reximi ⊢ ( ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) → ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑥 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑥 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑦 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑦 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑧 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) )
47 46 reximi ⊢ ( ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) → ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑥 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑥 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑦 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑦 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑧 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) )
48 ovex ⊢ ( 1 ..^ 2 ) ∈ V
49 48 mptex ⊢ ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ∈ V
50 f1eq1 ⊢ ( 𝑓 = ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) → ( 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ↔ ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) : ( 1 ..^ 2 ) –1-1→ 𝑃 ) )
51 nfmpt1 ⊢ Ⅎ 𝑗 ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 )
52 51 nfeq2 ⊢ Ⅎ 𝑗 𝑓 = ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 )
53 nfv ⊢ Ⅎ 𝑗 ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 )
54 52 53 nfan ⊢ Ⅎ 𝑗 ( 𝑓 = ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) )
55 simpll ⊢ ( ( ( 𝑓 = ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ 𝑗 ∈ ( 2 ..^ 2 ) ) → 𝑓 = ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) )
56 55 fveq1d ⊢ ( ( ( 𝑓 = ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ 𝑗 ∈ ( 2 ..^ 2 ) ) → ( 𝑓 ‘ 1 ) = ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) )
57 56 oveq1d ⊢ ( ( ( 𝑓 = ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ 𝑗 ∈ ( 2 ..^ 2 ) ) → ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑥 ) )
58 55 fveq1d ⊢ ( ( ( 𝑓 = ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ 𝑗 ∈ ( 2 ..^ 2 ) ) → ( 𝑓 ‘ 𝑗 ) = ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) )
59 58 oveq1d ⊢ ( ( ( 𝑓 = ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ 𝑗 ∈ ( 2 ..^ 2 ) ) → ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑥 ) )
60 57 59 eqeq12d ⊢ ( ( ( 𝑓 = ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ 𝑗 ∈ ( 2 ..^ 2 ) ) → ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ↔ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑥 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑥 ) ) )
61 56 oveq1d ⊢ ( ( ( 𝑓 = ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ 𝑗 ∈ ( 2 ..^ 2 ) ) → ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑦 ) )
62 58 oveq1d ⊢ ( ( ( 𝑓 = ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ 𝑗 ∈ ( 2 ..^ 2 ) ) → ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑦 ) )
63 61 62 eqeq12d ⊢ ( ( ( 𝑓 = ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ 𝑗 ∈ ( 2 ..^ 2 ) ) → ( ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ↔ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑦 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑦 ) ) )
64 56 oveq1d ⊢ ( ( ( 𝑓 = ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ 𝑗 ∈ ( 2 ..^ 2 ) ) → ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑧 ) )
65 58 oveq1d ⊢ ( ( ( 𝑓 = ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ 𝑗 ∈ ( 2 ..^ 2 ) ) → ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑧 ) )
66 64 65 eqeq12d ⊢ ( ( ( 𝑓 = ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ 𝑗 ∈ ( 2 ..^ 2 ) ) → ( ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ↔ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑧 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑧 ) ) )
67 60 63 66 3anbi123d ⊢ ( ( ( 𝑓 = ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ 𝑗 ∈ ( 2 ..^ 2 ) ) → ( ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ↔ ( ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑥 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑥 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑦 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑦 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑧 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑧 ) ) ) )
68 54 67 ralbida ⊢ ( ( 𝑓 = ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) → ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ↔ ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑥 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑥 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑦 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑦 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑧 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑧 ) ) ) )
69 68 anbi1d ⊢ ( ( 𝑓 = ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) → ( ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑥 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑥 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑦 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑦 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑧 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
70 69 2rexbidva ⊢ ( 𝑓 = ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) → ( ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑥 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑥 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑦 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑦 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑧 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
71 50 70 anbi12d ⊢ ( 𝑓 = ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) → ( ( 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ∧ ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) : ( 1 ..^ 2 ) –1-1→ 𝑃 ∧ ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑥 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑥 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑦 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑦 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑧 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
72 49 71 spcev ⊢ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) : ( 1 ..^ 2 ) –1-1→ 𝑃 ∧ ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑥 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑥 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑦 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑦 ) ∧ ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 1 ) − 𝑧 ) = ( ( ( 𝑗 ∈ ( 1 ..^ 2 ) ↦ 𝑥 ) ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) → ∃ 𝑓 ( 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ∧ ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
73 40 47 72 syl2an ⊢ ( ( 𝑥 ∈ 𝑃 ∧ ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) → ∃ 𝑓 ( 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ∧ ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
74 21 73 impbida ⊢ ( 𝑥 ∈ 𝑃 → ( ∃ 𝑓 ( 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ∧ ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) )
75 74 rexbiia ⊢ ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑓 ( 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ∧ ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) )
76 14 15 75 3bitr2i ⊢ ( ∃ 𝑓 ( 𝑓 : ( 1 ..^ 2 ) –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 2 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) )
77 8 76 bitrdi ⊢ ( 𝐺 ∈ 𝑉 → ( 𝐺 DimTarskiG≥ 2 ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) )