Metamath Proof Explorer

Theorem uspgrlimlem2

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

Ref Expression
Hypotheses uspgrlimlem1.m ⊢ 𝑀 = ( 𝐻 ClNeighbVtx 𝑋 )
uspgrlimlem1.j ⊢ 𝐽 = ( Edg ‘ 𝐻 )
uspgrlimlem1.l ⊢ 𝐿 = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 }
Assertion uspgrlimlem2 ( 𝐻 ∈ 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 f1ocnv ⊢ ( ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1-onto→ ( Edg ‘ 𝐻 ) → ◡ ( iEdg ‘ 𝐻 ) : ( Edg ‘ 𝐻 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) )
7 f1of ⊢ ( ◡ ( iEdg ‘ 𝐻 ) : ( Edg ‘ 𝐻 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) → ◡ ( iEdg ‘ 𝐻 ) : ( Edg ‘ 𝐻 ) ⟶ dom ( iEdg ‘ 𝐻 ) )
8 5 6 7 3syl ⊢ ( 𝐻 ∈ USPGraph → ◡ ( iEdg ‘ 𝐻 ) : ( Edg ‘ 𝐻 ) ⟶ dom ( iEdg ‘ 𝐻 ) )
9 2 rabeqi ⊢ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 } = { 𝑥 ∈ ( Edg ‘ 𝐻 ) ∣ 𝑥 ⊆ 𝑀 }
10 3 9 eqtri ⊢ 𝐿 = { 𝑥 ∈ ( Edg ‘ 𝐻 ) ∣ 𝑥 ⊆ 𝑀 }
11 10 ssrab3 ⊢ 𝐿 ⊆ ( Edg ‘ 𝐻 )
12 fimarab ⊢ ( ( ◡ ( iEdg ‘ 𝐻 ) : ( Edg ‘ 𝐻 ) ⟶ dom ( iEdg ‘ 𝐻 ) ∧ 𝐿 ⊆ ( Edg ‘ 𝐻 ) ) → ( ◡ ( iEdg ‘ 𝐻 ) “ 𝐿 ) = { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ∃ 𝑦 ∈ 𝐿 ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) = 𝑥 } )
13 8 11 12 sylancl ⊢ ( 𝐻 ∈ USPGraph → ( ◡ ( iEdg ‘ 𝐻 ) “ 𝐿 ) = { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ∃ 𝑦 ∈ 𝐿 ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) = 𝑥 } )
14 sseq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ 𝑀 ↔ 𝑦 ⊆ 𝑀 ) )
15 14 3 elrab2 ⊢ ( 𝑦 ∈ 𝐿 ↔ ( 𝑦 ∈ 𝐽 ∧ 𝑦 ⊆ 𝑀 ) )
16 2 eleq2i ⊢ ( 𝑦 ∈ 𝐽 ↔ 𝑦 ∈ ( Edg ‘ 𝐻 ) )
17 16 biimpi ⊢ ( 𝑦 ∈ 𝐽 → 𝑦 ∈ ( Edg ‘ 𝐻 ) )
18 f1ocnvfv2 ⊢ ( ( ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1-onto→ ( Edg ‘ 𝐻 ) ∧ 𝑦 ∈ ( Edg ‘ 𝐻 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) = 𝑦 )
19 5 17 18 syl2an ⊢ ( ( 𝐻 ∈ USPGraph ∧ 𝑦 ∈ 𝐽 ) → ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) = 𝑦 )
20 19 eqcomd ⊢ ( ( 𝐻 ∈ USPGraph ∧ 𝑦 ∈ 𝐽 ) → 𝑦 = ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) )
21 20 sseq1d ⊢ ( ( 𝐻 ∈ USPGraph ∧ 𝑦 ∈ 𝐽 ) → ( 𝑦 ⊆ 𝑀 ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) ⊆ 𝑀 ) )
22 21 biimpd ⊢ ( ( 𝐻 ∈ USPGraph ∧ 𝑦 ∈ 𝐽 ) → ( 𝑦 ⊆ 𝑀 → ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) ⊆ 𝑀 ) )
23 22 ex ⊢ ( 𝐻 ∈ USPGraph → ( 𝑦 ∈ 𝐽 → ( 𝑦 ⊆ 𝑀 → ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) ⊆ 𝑀 ) ) )
24 23 adantr ⊢ ( ( 𝐻 ∈ USPGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( 𝑦 ∈ 𝐽 → ( 𝑦 ⊆ 𝑀 → ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) ⊆ 𝑀 ) ) )
25 24 imp32 ⊢ ( ( ( 𝐻 ∈ USPGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑦 ⊆ 𝑀 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) ⊆ 𝑀 )
26 25 3adant3 ⊢ ( ( ( 𝐻 ∈ USPGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑦 ⊆ 𝑀 ) ∧ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) = 𝑥 ) → ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) ⊆ 𝑀 )
27 fveq2 ⊢ ( ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) )
28 27 sseq1d ⊢ ( ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) = 𝑥 → ( ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) ⊆ 𝑀 ↔ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 ) )
29 28 3ad2ant3 ⊢ ( ( ( 𝐻 ∈ USPGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑦 ⊆ 𝑀 ) ∧ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) = 𝑥 ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) ) ⊆ 𝑀 ↔ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 ) )
30 26 29 mpbid ⊢ ( ( ( 𝐻 ∈ USPGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑦 ⊆ 𝑀 ) ∧ ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) = 𝑥 ) → ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 )
31 30 3exp ⊢ ( ( 𝐻 ∈ USPGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ( 𝑦 ∈ 𝐽 ∧ 𝑦 ⊆ 𝑀 ) → ( ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 ) ) )
32 15 31 biimtrid ⊢ ( ( 𝐻 ∈ USPGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( 𝑦 ∈ 𝐿 → ( ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 ) ) )
33 32 rexlimdv ⊢ ( ( 𝐻 ∈ USPGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ∃ 𝑦 ∈ 𝐿 ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 ) )
34 fveqeq2 ⊢ ( 𝑦 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) → ( ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) = 𝑥 ↔ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ) = 𝑥 ) )
35 f1of ⊢ ( ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1-onto→ ( Edg ‘ 𝐻 ) → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) ⟶ ( Edg ‘ 𝐻 ) )
36 eqid ⊢ dom ( iEdg ‘ 𝐻 ) = dom ( iEdg ‘ 𝐻 )
37 2 eqcomi ⊢ ( Edg ‘ 𝐻 ) = 𝐽
38 36 37 feq23i ⊢ ( ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) ⟶ ( Edg ‘ 𝐻 ) ↔ ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) ⟶ 𝐽 )
39 38 biimpi ⊢ ( ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) ⟶ ( Edg ‘ 𝐻 ) → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) ⟶ 𝐽 )
40 5 35 39 3syl ⊢ ( 𝐻 ∈ USPGraph → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) ⟶ 𝐽 )
41 40 ffvelcdmda ⊢ ( ( 𝐻 ∈ USPGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ∈ 𝐽 )
42 41 anim1i ⊢ ( ( ( 𝐻 ∈ USPGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 ) → ( ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ∈ 𝐽 ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 ) )
43 sseq1 ⊢ ( 𝑦 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) → ( 𝑦 ⊆ 𝑀 ↔ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 ) )
44 14 43 3 elrab2w ⊢ ( ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ∈ 𝐿 ↔ ( ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ∈ 𝐽 ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 ) )
45 42 44 sylibr ⊢ ( ( ( 𝐻 ∈ USPGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 ) → ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ∈ 𝐿 )
46 f1ocnvfv1 ⊢ ( ( ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1-onto→ ( Edg ‘ 𝐻 ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ) = 𝑥 )
47 5 46 sylan ⊢ ( ( 𝐻 ∈ USPGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ) = 𝑥 )
48 47 adantr ⊢ ( ( ( 𝐻 ∈ USPGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 ) → ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ) = 𝑥 )
49 34 45 48 rspcedvdw ⊢ ( ( ( 𝐻 ∈ USPGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 ) → ∃ 𝑦 ∈ 𝐿 ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) = 𝑥 )
50 49 ex ⊢ ( ( 𝐻 ∈ USPGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 → ∃ 𝑦 ∈ 𝐿 ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) = 𝑥 ) )
51 33 50 impbid ⊢ ( ( 𝐻 ∈ USPGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ∃ 𝑦 ∈ 𝐿 ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) = 𝑥 ↔ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 ) )
52 51 rabbidva ⊢ ( 𝐻 ∈ USPGraph → { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ∃ 𝑦 ∈ 𝐿 ( ◡ ( iEdg ‘ 𝐻 ) ‘ 𝑦 ) = 𝑥 } = { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } )
53 13 52 eqtrd ⊢ ( 𝐻 ∈ USPGraph → ( ◡ ( iEdg ‘ 𝐻 ) “ 𝐿 ) = { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } )