MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ishlg Structured version   Visualization version   GIF version

Theorem ishlg 27833
Description: Rays : Definition 6.1 of [Schwabhauser] p. 43. With this definition, 𝐴(πΎβ€˜πΆ)𝐡 means that 𝐴 and 𝐡 are on the same ray with initial point 𝐢. 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., ((πΎβ€˜πΆ) β€œ {𝐴}). (Contributed by Thierry Arnoux, 21-Dec-2019.)
Hypotheses
Ref Expression
ishlg.p 𝑃 = (Baseβ€˜πΊ)
ishlg.i 𝐼 = (Itvβ€˜πΊ)
ishlg.k 𝐾 = (hlGβ€˜πΊ)
ishlg.a (πœ‘ β†’ 𝐴 ∈ 𝑃)
ishlg.b (πœ‘ β†’ 𝐡 ∈ 𝑃)
ishlg.c (πœ‘ β†’ 𝐢 ∈ 𝑃)
ishlg.g (πœ‘ β†’ 𝐺 ∈ 𝑉)
Assertion
Ref Expression
ishlg (πœ‘ β†’ (𝐴(πΎβ€˜πΆ)𝐡 ↔ (𝐴 β‰  𝐢 ∧ 𝐡 β‰  𝐢 ∧ (𝐴 ∈ (𝐢𝐼𝐡) ∨ 𝐡 ∈ (𝐢𝐼𝐴)))))

Proof of Theorem ishlg
Dummy variables π‘Ž 𝑏 𝑐 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 484 . . . . . 6 ((π‘Ž = 𝐴 ∧ 𝑏 = 𝐡) β†’ π‘Ž = 𝐴)
21neeq1d 3001 . . . . 5 ((π‘Ž = 𝐴 ∧ 𝑏 = 𝐡) β†’ (π‘Ž β‰  𝐢 ↔ 𝐴 β‰  𝐢))
3 simpr 486 . . . . . 6 ((π‘Ž = 𝐴 ∧ 𝑏 = 𝐡) β†’ 𝑏 = 𝐡)
43neeq1d 3001 . . . . 5 ((π‘Ž = 𝐴 ∧ 𝑏 = 𝐡) β†’ (𝑏 β‰  𝐢 ↔ 𝐡 β‰  𝐢))
53oveq2d 7420 . . . . . . 7 ((π‘Ž = 𝐴 ∧ 𝑏 = 𝐡) β†’ (𝐢𝐼𝑏) = (𝐢𝐼𝐡))
61, 5eleq12d 2828 . . . . . 6 ((π‘Ž = 𝐴 ∧ 𝑏 = 𝐡) β†’ (π‘Ž ∈ (𝐢𝐼𝑏) ↔ 𝐴 ∈ (𝐢𝐼𝐡)))
71oveq2d 7420 . . . . . . 7 ((π‘Ž = 𝐴 ∧ 𝑏 = 𝐡) β†’ (πΆπΌπ‘Ž) = (𝐢𝐼𝐴))
83, 7eleq12d 2828 . . . . . 6 ((π‘Ž = 𝐴 ∧ 𝑏 = 𝐡) β†’ (𝑏 ∈ (πΆπΌπ‘Ž) ↔ 𝐡 ∈ (𝐢𝐼𝐴)))
96, 8orbi12d 918 . . . . 5 ((π‘Ž = 𝐴 ∧ 𝑏 = 𝐡) β†’ ((π‘Ž ∈ (𝐢𝐼𝑏) ∨ 𝑏 ∈ (πΆπΌπ‘Ž)) ↔ (𝐴 ∈ (𝐢𝐼𝐡) ∨ 𝐡 ∈ (𝐢𝐼𝐴))))
102, 4, 93anbi123d 1437 . . . 4 ((π‘Ž = 𝐴 ∧ 𝑏 = 𝐡) β†’ ((π‘Ž β‰  𝐢 ∧ 𝑏 β‰  𝐢 ∧ (π‘Ž ∈ (𝐢𝐼𝑏) ∨ 𝑏 ∈ (πΆπΌπ‘Ž))) ↔ (𝐴 β‰  𝐢 ∧ 𝐡 β‰  𝐢 ∧ (𝐴 ∈ (𝐢𝐼𝐡) ∨ 𝐡 ∈ (𝐢𝐼𝐴)))))
11 eqid 2733 . . . 4 {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (π‘Ž β‰  𝐢 ∧ 𝑏 β‰  𝐢 ∧ (π‘Ž ∈ (𝐢𝐼𝑏) ∨ 𝑏 ∈ (πΆπΌπ‘Ž))))} = {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (π‘Ž β‰  𝐢 ∧ 𝑏 β‰  𝐢 ∧ (π‘Ž ∈ (𝐢𝐼𝑏) ∨ 𝑏 ∈ (πΆπΌπ‘Ž))))}
1210, 11brab2a 5767 . . 3 (𝐴{βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (π‘Ž β‰  𝐢 ∧ 𝑏 β‰  𝐢 ∧ (π‘Ž ∈ (𝐢𝐼𝑏) ∨ 𝑏 ∈ (πΆπΌπ‘Ž))))}𝐡 ↔ ((𝐴 ∈ 𝑃 ∧ 𝐡 ∈ 𝑃) ∧ (𝐴 β‰  𝐢 ∧ 𝐡 β‰  𝐢 ∧ (𝐴 ∈ (𝐢𝐼𝐡) ∨ 𝐡 ∈ (𝐢𝐼𝐴)))))
1312a1i 11 . 2 (πœ‘ β†’ (𝐴{βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (π‘Ž β‰  𝐢 ∧ 𝑏 β‰  𝐢 ∧ (π‘Ž ∈ (𝐢𝐼𝑏) ∨ 𝑏 ∈ (πΆπΌπ‘Ž))))}𝐡 ↔ ((𝐴 ∈ 𝑃 ∧ 𝐡 ∈ 𝑃) ∧ (𝐴 β‰  𝐢 ∧ 𝐡 β‰  𝐢 ∧ (𝐴 ∈ (𝐢𝐼𝐡) ∨ 𝐡 ∈ (𝐢𝐼𝐴))))))
14 ishlg.k . . . . 5 𝐾 = (hlGβ€˜πΊ)
15 ishlg.g . . . . . 6 (πœ‘ β†’ 𝐺 ∈ 𝑉)
16 elex 3493 . . . . . 6 (𝐺 ∈ 𝑉 β†’ 𝐺 ∈ V)
17 fveq2 6888 . . . . . . . . 9 (𝑔 = 𝐺 β†’ (Baseβ€˜π‘”) = (Baseβ€˜πΊ))
18 ishlg.p . . . . . . . . 9 𝑃 = (Baseβ€˜πΊ)
1917, 18eqtr4di 2791 . . . . . . . 8 (𝑔 = 𝐺 β†’ (Baseβ€˜π‘”) = 𝑃)
2019eleq2d 2820 . . . . . . . . . . 11 (𝑔 = 𝐺 β†’ (π‘Ž ∈ (Baseβ€˜π‘”) ↔ π‘Ž ∈ 𝑃))
2119eleq2d 2820 . . . . . . . . . . 11 (𝑔 = 𝐺 β†’ (𝑏 ∈ (Baseβ€˜π‘”) ↔ 𝑏 ∈ 𝑃))
2220, 21anbi12d 632 . . . . . . . . . 10 (𝑔 = 𝐺 β†’ ((π‘Ž ∈ (Baseβ€˜π‘”) ∧ 𝑏 ∈ (Baseβ€˜π‘”)) ↔ (π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)))
23 fveq2 6888 . . . . . . . . . . . . . . 15 (𝑔 = 𝐺 β†’ (Itvβ€˜π‘”) = (Itvβ€˜πΊ))
24 ishlg.i . . . . . . . . . . . . . . 15 𝐼 = (Itvβ€˜πΊ)
2523, 24eqtr4di 2791 . . . . . . . . . . . . . 14 (𝑔 = 𝐺 β†’ (Itvβ€˜π‘”) = 𝐼)
2625oveqd 7421 . . . . . . . . . . . . 13 (𝑔 = 𝐺 β†’ (𝑐(Itvβ€˜π‘”)𝑏) = (𝑐𝐼𝑏))
2726eleq2d 2820 . . . . . . . . . . . 12 (𝑔 = 𝐺 β†’ (π‘Ž ∈ (𝑐(Itvβ€˜π‘”)𝑏) ↔ π‘Ž ∈ (𝑐𝐼𝑏)))
2825oveqd 7421 . . . . . . . . . . . . 13 (𝑔 = 𝐺 β†’ (𝑐(Itvβ€˜π‘”)π‘Ž) = (π‘πΌπ‘Ž))
2928eleq2d 2820 . . . . . . . . . . . 12 (𝑔 = 𝐺 β†’ (𝑏 ∈ (𝑐(Itvβ€˜π‘”)π‘Ž) ↔ 𝑏 ∈ (π‘πΌπ‘Ž)))
3027, 29orbi12d 918 . . . . . . . . . . 11 (𝑔 = 𝐺 β†’ ((π‘Ž ∈ (𝑐(Itvβ€˜π‘”)𝑏) ∨ 𝑏 ∈ (𝑐(Itvβ€˜π‘”)π‘Ž)) ↔ (π‘Ž ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (π‘πΌπ‘Ž))))
31303anbi3d 1443 . . . . . . . . . 10 (𝑔 = 𝐺 β†’ ((π‘Ž β‰  𝑐 ∧ 𝑏 β‰  𝑐 ∧ (π‘Ž ∈ (𝑐(Itvβ€˜π‘”)𝑏) ∨ 𝑏 ∈ (𝑐(Itvβ€˜π‘”)π‘Ž))) ↔ (π‘Ž β‰  𝑐 ∧ 𝑏 β‰  𝑐 ∧ (π‘Ž ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (π‘πΌπ‘Ž)))))
3222, 31anbi12d 632 . . . . . . . . 9 (𝑔 = 𝐺 β†’ (((π‘Ž ∈ (Baseβ€˜π‘”) ∧ 𝑏 ∈ (Baseβ€˜π‘”)) ∧ (π‘Ž β‰  𝑐 ∧ 𝑏 β‰  𝑐 ∧ (π‘Ž ∈ (𝑐(Itvβ€˜π‘”)𝑏) ∨ 𝑏 ∈ (𝑐(Itvβ€˜π‘”)π‘Ž)))) ↔ ((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (π‘Ž β‰  𝑐 ∧ 𝑏 β‰  𝑐 ∧ (π‘Ž ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (π‘πΌπ‘Ž))))))
3332opabbidv 5213 . . . . . . . 8 (𝑔 = 𝐺 β†’ {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (Baseβ€˜π‘”) ∧ 𝑏 ∈ (Baseβ€˜π‘”)) ∧ (π‘Ž β‰  𝑐 ∧ 𝑏 β‰  𝑐 ∧ (π‘Ž ∈ (𝑐(Itvβ€˜π‘”)𝑏) ∨ 𝑏 ∈ (𝑐(Itvβ€˜π‘”)π‘Ž))))} = {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (π‘Ž β‰  𝑐 ∧ 𝑏 β‰  𝑐 ∧ (π‘Ž ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (π‘πΌπ‘Ž))))})
3419, 33mpteq12dv 5238 . . . . . . 7 (𝑔 = 𝐺 β†’ (𝑐 ∈ (Baseβ€˜π‘”) ↦ {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (Baseβ€˜π‘”) ∧ 𝑏 ∈ (Baseβ€˜π‘”)) ∧ (π‘Ž β‰  𝑐 ∧ 𝑏 β‰  𝑐 ∧ (π‘Ž ∈ (𝑐(Itvβ€˜π‘”)𝑏) ∨ 𝑏 ∈ (𝑐(Itvβ€˜π‘”)π‘Ž))))}) = (𝑐 ∈ 𝑃 ↦ {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (π‘Ž β‰  𝑐 ∧ 𝑏 β‰  𝑐 ∧ (π‘Ž ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (π‘πΌπ‘Ž))))}))
35 df-hlg 27832 . . . . . . 7 hlG = (𝑔 ∈ V ↦ (𝑐 ∈ (Baseβ€˜π‘”) ↦ {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (Baseβ€˜π‘”) ∧ 𝑏 ∈ (Baseβ€˜π‘”)) ∧ (π‘Ž β‰  𝑐 ∧ 𝑏 β‰  𝑐 ∧ (π‘Ž ∈ (𝑐(Itvβ€˜π‘”)𝑏) ∨ 𝑏 ∈ (𝑐(Itvβ€˜π‘”)π‘Ž))))}))
3634, 35, 18mptfvmpt 7225 . . . . . 6 (𝐺 ∈ V β†’ (hlGβ€˜πΊ) = (𝑐 ∈ 𝑃 ↦ {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (π‘Ž β‰  𝑐 ∧ 𝑏 β‰  𝑐 ∧ (π‘Ž ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (π‘πΌπ‘Ž))))}))
3715, 16, 363syl 18 . . . . 5 (πœ‘ β†’ (hlGβ€˜πΊ) = (𝑐 ∈ 𝑃 ↦ {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (π‘Ž β‰  𝑐 ∧ 𝑏 β‰  𝑐 ∧ (π‘Ž ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (π‘πΌπ‘Ž))))}))
3814, 37eqtrid 2785 . . . 4 (πœ‘ β†’ 𝐾 = (𝑐 ∈ 𝑃 ↦ {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (π‘Ž β‰  𝑐 ∧ 𝑏 β‰  𝑐 ∧ (π‘Ž ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (π‘πΌπ‘Ž))))}))
39 neeq2 3005 . . . . . . . 8 (𝑐 = 𝐢 β†’ (π‘Ž β‰  𝑐 ↔ π‘Ž β‰  𝐢))
40 neeq2 3005 . . . . . . . 8 (𝑐 = 𝐢 β†’ (𝑏 β‰  𝑐 ↔ 𝑏 β‰  𝐢))
41 oveq1 7411 . . . . . . . . . 10 (𝑐 = 𝐢 β†’ (𝑐𝐼𝑏) = (𝐢𝐼𝑏))
4241eleq2d 2820 . . . . . . . . 9 (𝑐 = 𝐢 β†’ (π‘Ž ∈ (𝑐𝐼𝑏) ↔ π‘Ž ∈ (𝐢𝐼𝑏)))
43 oveq1 7411 . . . . . . . . . 10 (𝑐 = 𝐢 β†’ (π‘πΌπ‘Ž) = (πΆπΌπ‘Ž))
4443eleq2d 2820 . . . . . . . . 9 (𝑐 = 𝐢 β†’ (𝑏 ∈ (π‘πΌπ‘Ž) ↔ 𝑏 ∈ (πΆπΌπ‘Ž)))
4542, 44orbi12d 918 . . . . . . . 8 (𝑐 = 𝐢 β†’ ((π‘Ž ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (π‘πΌπ‘Ž)) ↔ (π‘Ž ∈ (𝐢𝐼𝑏) ∨ 𝑏 ∈ (πΆπΌπ‘Ž))))
4639, 40, 453anbi123d 1437 . . . . . . 7 (𝑐 = 𝐢 β†’ ((π‘Ž β‰  𝑐 ∧ 𝑏 β‰  𝑐 ∧ (π‘Ž ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (π‘πΌπ‘Ž))) ↔ (π‘Ž β‰  𝐢 ∧ 𝑏 β‰  𝐢 ∧ (π‘Ž ∈ (𝐢𝐼𝑏) ∨ 𝑏 ∈ (πΆπΌπ‘Ž)))))
4746anbi2d 630 . . . . . 6 (𝑐 = 𝐢 β†’ (((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (π‘Ž β‰  𝑐 ∧ 𝑏 β‰  𝑐 ∧ (π‘Ž ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (π‘πΌπ‘Ž)))) ↔ ((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (π‘Ž β‰  𝐢 ∧ 𝑏 β‰  𝐢 ∧ (π‘Ž ∈ (𝐢𝐼𝑏) ∨ 𝑏 ∈ (πΆπΌπ‘Ž))))))
4847opabbidv 5213 . . . . 5 (𝑐 = 𝐢 β†’ {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (π‘Ž β‰  𝑐 ∧ 𝑏 β‰  𝑐 ∧ (π‘Ž ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (π‘πΌπ‘Ž))))} = {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (π‘Ž β‰  𝐢 ∧ 𝑏 β‰  𝐢 ∧ (π‘Ž ∈ (𝐢𝐼𝑏) ∨ 𝑏 ∈ (πΆπΌπ‘Ž))))})
4948adantl 483 . . . 4 ((πœ‘ ∧ 𝑐 = 𝐢) β†’ {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (π‘Ž β‰  𝑐 ∧ 𝑏 β‰  𝑐 ∧ (π‘Ž ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (π‘πΌπ‘Ž))))} = {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (π‘Ž β‰  𝐢 ∧ 𝑏 β‰  𝐢 ∧ (π‘Ž ∈ (𝐢𝐼𝑏) ∨ 𝑏 ∈ (πΆπΌπ‘Ž))))})
50 ishlg.c . . . 4 (πœ‘ β†’ 𝐢 ∈ 𝑃)
5118fvexi 6902 . . . . . . 7 𝑃 ∈ V
5251, 51xpex 7735 . . . . . 6 (𝑃 Γ— 𝑃) ∈ V
53 opabssxp 5766 . . . . . 6 {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (π‘Ž β‰  𝐢 ∧ 𝑏 β‰  𝐢 ∧ (π‘Ž ∈ (𝐢𝐼𝑏) ∨ 𝑏 ∈ (πΆπΌπ‘Ž))))} βŠ† (𝑃 Γ— 𝑃)
5452, 53ssexi 5321 . . . . 5 {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (π‘Ž β‰  𝐢 ∧ 𝑏 β‰  𝐢 ∧ (π‘Ž ∈ (𝐢𝐼𝑏) ∨ 𝑏 ∈ (πΆπΌπ‘Ž))))} ∈ V
5554a1i 11 . . . 4 (πœ‘ β†’ {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (π‘Ž β‰  𝐢 ∧ 𝑏 β‰  𝐢 ∧ (π‘Ž ∈ (𝐢𝐼𝑏) ∨ 𝑏 ∈ (πΆπΌπ‘Ž))))} ∈ V)
5638, 49, 50, 55fvmptd 7001 . . 3 (πœ‘ β†’ (πΎβ€˜πΆ) = {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (π‘Ž β‰  𝐢 ∧ 𝑏 β‰  𝐢 ∧ (π‘Ž ∈ (𝐢𝐼𝑏) ∨ 𝑏 ∈ (πΆπΌπ‘Ž))))})
5756breqd 5158 . 2 (πœ‘ β†’ (𝐴(πΎβ€˜πΆ)𝐡 ↔ 𝐴{βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (π‘Ž β‰  𝐢 ∧ 𝑏 β‰  𝐢 ∧ (π‘Ž ∈ (𝐢𝐼𝑏) ∨ 𝑏 ∈ (πΆπΌπ‘Ž))))}𝐡))
58 ishlg.a . . . 4 (πœ‘ β†’ 𝐴 ∈ 𝑃)
59 ishlg.b . . . 4 (πœ‘ β†’ 𝐡 ∈ 𝑃)
6058, 59jca 513 . . 3 (πœ‘ β†’ (𝐴 ∈ 𝑃 ∧ 𝐡 ∈ 𝑃))
6160biantrurd 534 . 2 (πœ‘ β†’ ((𝐴 β‰  𝐢 ∧ 𝐡 β‰  𝐢 ∧ (𝐴 ∈ (𝐢𝐼𝐡) ∨ 𝐡 ∈ (𝐢𝐼𝐴))) ↔ ((𝐴 ∈ 𝑃 ∧ 𝐡 ∈ 𝑃) ∧ (𝐴 β‰  𝐢 ∧ 𝐡 β‰  𝐢 ∧ (𝐴 ∈ (𝐢𝐼𝐡) ∨ 𝐡 ∈ (𝐢𝐼𝐴))))))
6213, 57, 613bitr4d 311 1 (πœ‘ β†’ (𝐴(πΎβ€˜πΆ)𝐡 ↔ (𝐴 β‰  𝐢 ∧ 𝐡 β‰  𝐢 ∧ (𝐴 ∈ (𝐢𝐼𝐡) ∨ 𝐡 ∈ (𝐢𝐼𝐴)))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  Vcvv 3475   class class class wbr 5147  {copab 5209   ↦ cmpt 5230   Γ— cxp 5673  β€˜cfv 6540  (class class class)co 7404  Basecbs 17140  Itvcitv 27664  hlGchlg 27831
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7407  df-hlg 27832
This theorem is referenced by:  hlcomb  27834  hlne1  27836  hlne2  27837  hlln  27838  hlid  27840  hltr  27841  hlbtwn  27842  btwnhl1  27843  btwnhl2  27844  btwnhl  27845  lnhl  27846  hlcgrex  27847  mirhl  27910  mirbtwnhl  27911  mirhl2  27912  opphllem4  27981  opphl  27985  hlpasch  27987  lnopp2hpgb  27994  cgracgr  28049  cgraswap  28051  flatcgra  28055  cgrahl  28058  cgracol  28059
  Copyright terms: Public domain W3C validator