Metamath Proof Explorer

Theorem ishlg

Description: Rays : Definition 6.1 of Schwabhauser p. 43. With this definition, A ( KC ) B means that A and B are on the same ray with initial point C . This follows the same notation as Schwabhauser where rays are first defined as a relation. It is possible to recover the ray itself using e.g., ( ( KC ) " { A } ) . (Contributed by Thierry Arnoux, 21-Dec-2019)

Ref Expression
Hypotheses ishlg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
ishlg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
ishlg.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
ishlg.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
ishlg.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
ishlg.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
ishlg.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
Assertion ishlg ( 𝜑 → ( 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ↔ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ishlg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 ishlg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 ishlg.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 ishlg.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
5 ishlg.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
6 ishlg.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
7 ishlg.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
8 simpl ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → 𝑎 = 𝐴 )
9 8 neeq1d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑎 ≠ 𝐶 ↔ 𝐴 ≠ 𝐶 ) )
10 simpr ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
11 10 neeq1d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑏 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶 ) )
12 10 oveq2d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝐶 𝐼 𝑏 ) = ( 𝐶 𝐼 𝐵 ) )
13 8 12 eleq12d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ↔ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) )
14 8 oveq2d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝐶 𝐼 𝑎 ) = ( 𝐶 𝐼 𝐴 ) )
15 10 14 eleq12d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ↔ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) )
16 13 15 orbi12d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ↔ ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ) )
17 9 11 16 3anbi123d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ↔ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ) ) )
18 eqid ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) }
19 17 18 brab2a ⊢ ( 𝐴 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) } 𝐵 ↔ ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ) ) )
20 19 a1i ⊢ ( 𝜑 → ( 𝐴 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) } 𝐵 ↔ ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ) ) ) )
21 elex ⊢ ( 𝐺 ∈ 𝑉 → 𝐺 ∈ V )
22 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
23 22 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝑃 )
24 23 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↔ 𝑎 ∈ 𝑃 ) )
25 23 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑏 ∈ ( Base ‘ 𝑔 ) ↔ 𝑏 ∈ 𝑃 ) )
26 24 25 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑎 ∈ ( Base ‘ 𝑔 ) ∧ 𝑏 ∈ ( Base ‘ 𝑔 ) ) ↔ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) )
27 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Itv ‘ 𝑔 ) = ( Itv ‘ 𝐺 ) )
28 27 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Itv ‘ 𝑔 ) = 𝐼 )
29 28 oveqd ⊢ ( 𝑔 = 𝐺 → ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) = ( 𝑐 𝐼 𝑏 ) )
30 29 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) ↔ 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ) )
31 28 oveqd ⊢ ( 𝑔 = 𝐺 → ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) = ( 𝑐 𝐼 𝑎 ) )
32 31 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) ↔ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) )
33 30 32 orbi12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) ) ↔ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) )
34 33 3anbi3d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ↔ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) ) )
35 26 34 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑎 ∈ ( Base ‘ 𝑔 ) ∧ 𝑏 ∈ ( Base ‘ 𝑔 ) ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) ↔ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) ) ) )
36 35 opabbidv ⊢ ( 𝑔 = 𝐺 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( Base ‘ 𝑔 ) ∧ 𝑏 ∈ ( Base ‘ 𝑔 ) ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) ) } )
37 23 36 mpteq12dv ⊢ ( 𝑔 = 𝐺 → ( 𝑐 ∈ ( Base ‘ 𝑔 ) ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( Base ‘ 𝑔 ) ∧ 𝑏 ∈ ( Base ‘ 𝑔 ) ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) } ) = ( 𝑐 ∈ 𝑃 ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) ) } ) )
38 df-hlg ⊢ hlG = ( 𝑔 ∈ V ↦ ( 𝑐 ∈ ( Base ‘ 𝑔 ) ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( Base ‘ 𝑔 ) ∧ 𝑏 ∈ ( Base ‘ 𝑔 ) ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) } ) )
39 37 38 1 mptfvmpt ⊢ ( 𝐺 ∈ V → ( hlG ‘ 𝐺 ) = ( 𝑐 ∈ 𝑃 ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) ) } ) )
40 7 21 39 3syl ⊢ ( 𝜑 → ( hlG ‘ 𝐺 ) = ( 𝑐 ∈ 𝑃 ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) ) } ) )
41 3 40 syl5eq ⊢ ( 𝜑 → 𝐾 = ( 𝑐 ∈ 𝑃 ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) ) } ) )
42 neeq2 ⊢ ( 𝑐 = 𝐶 → ( 𝑎 ≠ 𝑐 ↔ 𝑎 ≠ 𝐶 ) )
43 neeq2 ⊢ ( 𝑐 = 𝐶 → ( 𝑏 ≠ 𝑐 ↔ 𝑏 ≠ 𝐶 ) )
44 oveq1 ⊢ ( 𝑐 = 𝐶 → ( 𝑐 𝐼 𝑏 ) = ( 𝐶 𝐼 𝑏 ) )
45 44 eleq2d ⊢ ( 𝑐 = 𝐶 → ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ↔ 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ) )
46 oveq1 ⊢ ( 𝑐 = 𝐶 → ( 𝑐 𝐼 𝑎 ) = ( 𝐶 𝐼 𝑎 ) )
47 46 eleq2d ⊢ ( 𝑐 = 𝐶 → ( 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ↔ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) )
48 45 47 orbi12d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ↔ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) )
49 42 43 48 3anbi123d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) ↔ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) )
50 49 anbi2d ⊢ ( 𝑐 = 𝐶 → ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) ) ↔ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) ) )
51 50 opabbidv ⊢ ( 𝑐 = 𝐶 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) } )
52 51 adantl ⊢ ( ( 𝜑 ∧ 𝑐 = 𝐶 ) → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) } )
53 1 fvexi ⊢ 𝑃 ∈ V
54 53 53 xpex ⊢ ( 𝑃 × 𝑃 ) ∈ V
55 opabssxp ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) } ⊆ ( 𝑃 × 𝑃 )
56 54 55 ssexi ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) } ∈ V
57 56 a1i ⊢ ( 𝜑 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) } ∈ V )
58 41 52 6 57 fvmptd ⊢ ( 𝜑 → ( 𝐾 ‘ 𝐶 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) } )
59 58 breqd ⊢ ( 𝜑 → ( 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ↔ 𝐴 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) } 𝐵 ) )
60 4 5 jca ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) )
61 60 biantrurd ⊢ ( 𝜑 → ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ) ↔ ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ) ) ) )
62 20 59 61 3bitr4d ⊢ ( 𝜑 → ( 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ↔ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ) ) )