This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uspgrlimlem1

Description: Lemma 1 for uspgrlim . (Contributed by AV, 16-Aug-2025)

Ref Expression
Hypotheses uspgrlimlem1.m ⊢ 𝑀 = ( 𝐻 ClNeighbVtx 𝑋 )
uspgrlimlem1.j ⊢ 𝐽 = ( Edg ‘ 𝐻 )
uspgrlimlem1.l ⊢ 𝐿 = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 }
Assertion uspgrlimlem1 ( 𝐻 ∈ USPGraph → 𝐿 = ( ( iEdg ‘ 𝐻 ) “ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ) )

Proof

Step Hyp Ref Expression
1 uspgrlimlem1.m ⊢ 𝑀 = ( 𝐻 ClNeighbVtx 𝑋 )
2 uspgrlimlem1.j ⊢ 𝐽 = ( Edg ‘ 𝐻 )
3 uspgrlimlem1.l ⊢ 𝐿 = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 }
4 eqid ⊢ ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐻 )
5 4 uspgrf1oedg ⊢ ( 𝐻 ∈ USPGraph → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1-onto→ ( Edg ‘ 𝐻 ) )
6 f1of ⊢ ( ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1-onto→ ( Edg ‘ 𝐻 ) → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) ⟶ ( Edg ‘ 𝐻 ) )
7 5 6 syl ⊢ ( 𝐻 ∈ USPGraph → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) ⟶ ( Edg ‘ 𝐻 ) )
8 ssrab2 ⊢ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ⊆ dom ( iEdg ‘ 𝐻 )
9 fimarab ⊢ ( ( ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) ⟶ ( Edg ‘ 𝐻 ) ∧ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ⊆ dom ( iEdg ‘ 𝐻 ) ) → ( ( iEdg ‘ 𝐻 ) “ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ) = { 𝑦 ∈ ( Edg ‘ 𝐻 ) ∣ ∃ 𝑧 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ( ( iEdg ‘ 𝐻 ) ‘ 𝑧 ) = 𝑦 } )
10 7 8 9 sylancl ⊢ ( 𝐻 ∈ USPGraph → ( ( iEdg ‘ 𝐻 ) “ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ) = { 𝑦 ∈ ( Edg ‘ 𝐻 ) ∣ ∃ 𝑧 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ( ( iEdg ‘ 𝐻 ) ‘ 𝑧 ) = 𝑦 } )
11 2 eqcomi ⊢ ( Edg ‘ 𝐻 ) = 𝐽
12 11 a1i ⊢ ( 𝐻 ∈ USPGraph → ( Edg ‘ 𝐻 ) = 𝐽 )
13 fveq2 ⊢ ( 𝑥 = 𝑧 → ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑧 ) )
14 13 sseq1d ⊢ ( 𝑥 = 𝑧 → ( ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 ↔ ( ( iEdg ‘ 𝐻 ) ‘ 𝑧 ) ⊆ 𝑀 ) )
15 14 rexrab ⊢ ( ∃ 𝑧 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ( ( iEdg ‘ 𝐻 ) ‘ 𝑧 ) = 𝑦 ↔ ∃ 𝑧 ∈ dom ( iEdg ‘ 𝐻 ) ( ( ( iEdg ‘ 𝐻 ) ‘ 𝑧 ) ⊆ 𝑀 ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑧 ) = 𝑦 ) )
16 sseq1 ⊢ ( ( ( iEdg ‘ 𝐻 ) ‘ 𝑧 ) = 𝑦 → ( ( ( iEdg ‘ 𝐻 ) ‘ 𝑧 ) ⊆ 𝑀 ↔ 𝑦 ⊆ 𝑀 ) )
17 16 biimpac ⊢ ( ( ( ( iEdg ‘ 𝐻 ) ‘ 𝑧 ) ⊆ 𝑀 ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑧 ) = 𝑦 ) → 𝑦 ⊆ 𝑀 )
18 17 a1i ⊢ ( ( ( 𝐻 ∈ USPGraph ∧ 𝑦 ∈ ( Edg ‘ 𝐻 ) ) ∧ 𝑧 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ( ( ( iEdg ‘ 𝐻 ) ‘ 𝑧 ) ⊆ 𝑀 ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑧 ) = 𝑦 ) → 𝑦 ⊆ 𝑀 ) )
19 f1ocnv ⊢ ( ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1-onto→ ( Edg ‘ 𝐻 ) → ◡ ( iEdg ‘ 𝐻 ) : ( Edg ‘ 𝐻 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) )
20 f1of ⊢ ( ◡ ( iEdg ‘ 𝐻 ) : ( Edg ‘ 𝐻 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) → ◡ ( iEdg ‘ 𝐻 ) : ( Edg ‘ 𝐻 ) ⟶ dom ( iEdg ‘ 𝐻 ) )
21 5 19 20 3syl ⊢ ( 𝐻 ∈ USPGraph → ◡ ( iEdg ‘ 𝐻 ) : ( Edg ‘ 𝐻 ) ⟶ dom ( iEdg ‘ 𝐻 ) )
22 21 ffvelcdmda ⊢ ( ( 𝐻 ∈ USPGraph ∧ 𝑦 ∈ ( Edg ‘ 𝐻 ) ) → ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐻 ) )
23 22 adantr ⊢ ( ( ( 𝐻 ∈ USPGraph ∧ 𝑦 ∈ ( Edg ‘ 𝐻 ) ) ∧ 𝑦 ⊆ 𝑀 ) → ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐻 ) )
24 f1ocnvfv2 ⊢ ( ( ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1-onto→ ( Edg ‘ 𝐻 ) ∧ 𝑦 ∈ ( Edg ‘ 𝐻 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) = 𝑦 )
25 5 24 sylan ⊢ ( ( 𝐻 ∈ USPGraph ∧ 𝑦 ∈ ( Edg ‘ 𝐻 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) = 𝑦 )
26 25 adantr ⊢ ( ( ( 𝐻 ∈ USPGraph ∧ 𝑦 ∈ ( Edg ‘ 𝐻 ) ) ∧ 𝑦 ⊆ 𝑀 ) → ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) = 𝑦 )
27 sseq1 ⊢ ( 𝑦 = ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) → ( 𝑦 ⊆ 𝑀 ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) ⊆ 𝑀 ) )
28 27 eqcoms ⊢ ( ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) = 𝑦 → ( 𝑦 ⊆ 𝑀 ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) ⊆ 𝑀 ) )
29 28 biimpcd ⊢ ( 𝑦 ⊆ 𝑀 → ( ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) = 𝑦 → ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) ⊆ 𝑀 ) )
30 29 adantl ⊢ ( ( ( 𝐻 ∈ USPGraph ∧ 𝑦 ∈ ( Edg ‘ 𝐻 ) ) ∧ 𝑦 ⊆ 𝑀 ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) = 𝑦 → ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) ⊆ 𝑀 ) )
31 30 ancrd ⊢ ( ( ( 𝐻 ∈ USPGraph ∧ 𝑦 ∈ ( Edg ‘ 𝐻 ) ) ∧ 𝑦 ⊆ 𝑀 ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) = 𝑦 → ( ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) ⊆ 𝑀 ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) = 𝑦 ) ) )
32 26 31 mpd ⊢ ( ( ( 𝐻 ∈ USPGraph ∧ 𝑦 ∈ ( Edg ‘ 𝐻 ) ) ∧ 𝑦 ⊆ 𝑀 ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) ⊆ 𝑀 ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) = 𝑦 ) )
33 fveq2 ⊢ ( 𝑧 = ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) → ( ( iEdg ‘ 𝐻 ) ‘ 𝑧 ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) )
34 33 sseq1d ⊢ ( 𝑧 = ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) → ( ( ( iEdg ‘ 𝐻 ) ‘ 𝑧 ) ⊆ 𝑀 ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) ⊆ 𝑀 ) )
35 fveqeq2 ⊢ ( 𝑧 = ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) → ( ( ( iEdg ‘ 𝐻 ) ‘ 𝑧 ) = 𝑦 ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) = 𝑦 ) )
36 34 35 anbi12d ⊢ ( 𝑧 = ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) → ( ( ( ( iEdg ‘ 𝐻 ) ‘ 𝑧 ) ⊆ 𝑀 ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑧 ) = 𝑦 ) ↔ ( ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) ⊆ 𝑀 ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) = 𝑦 ) ) )
37 18 23 32 36 rspceb2dv ⊢ ( ( 𝐻 ∈ USPGraph ∧ 𝑦 ∈ ( Edg ‘ 𝐻 ) ) → ( ∃ 𝑧 ∈ dom ( iEdg ‘ 𝐻 ) ( ( ( iEdg ‘ 𝐻 ) ‘ 𝑧 ) ⊆ 𝑀 ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑧 ) = 𝑦 ) ↔ 𝑦 ⊆ 𝑀 ) )
38 15 37 bitrid ⊢ ( ( 𝐻 ∈ USPGraph ∧ 𝑦 ∈ ( Edg ‘ 𝐻 ) ) → ( ∃ 𝑧 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ( ( iEdg ‘ 𝐻 ) ‘ 𝑧 ) = 𝑦 ↔ 𝑦 ⊆ 𝑀 ) )
39 12 38 rabeqbidva ⊢ ( 𝐻 ∈ USPGraph → { 𝑦 ∈ ( Edg ‘ 𝐻 ) ∣ ∃ 𝑧 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ( ( iEdg ‘ 𝐻 ) ‘ 𝑧 ) = 𝑦 } = { 𝑦 ∈ 𝐽 ∣ 𝑦 ⊆ 𝑀 } )
40 sseq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ⊆ 𝑀 ↔ 𝑥 ⊆ 𝑀 ) )
41 40 cbvrabv ⊢ { 𝑦 ∈ 𝐽 ∣ 𝑦 ⊆ 𝑀 } = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 }
42 41 a1i ⊢ ( 𝐻 ∈ USPGraph → { 𝑦 ∈ 𝐽 ∣ 𝑦 ⊆ 𝑀 } = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 } )
43 10 39 42 3eqtrrd ⊢ ( 𝐻 ∈ USPGraph → { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 } = ( ( iEdg ‘ 𝐻 ) “ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ) )
44 3 43 eqtrid ⊢ ( 𝐻 ∈ USPGraph → 𝐿 = ( ( iEdg ‘ 𝐻 ) “ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ) )