Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pwrssmgc Structured version   Visualization version   GIF version

Theorem pwrssmgc 31902
Description: Given a function 𝐹, exhibit a Galois connection between subsets of its domain and subsets of its range. (Contributed by Thierry Arnoux, 26-Apr-2024.)
Hypotheses
Ref Expression
pwrssmgc.1 𝐺 = (𝑛 ∈ 𝒫 π‘Œ ↦ (◑𝐹 β€œ 𝑛))
pwrssmgc.2 𝐻 = (π‘š ∈ 𝒫 𝑋 ↦ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† π‘š})
pwrssmgc.3 𝑉 = (toIncβ€˜π’« π‘Œ)
pwrssmgc.4 π‘Š = (toIncβ€˜π’« 𝑋)
pwrssmgc.5 (πœ‘ β†’ 𝑋 ∈ 𝐴)
pwrssmgc.6 (πœ‘ β†’ π‘Œ ∈ 𝐡)
pwrssmgc.7 (πœ‘ β†’ 𝐹:π‘‹βŸΆπ‘Œ)
Assertion
Ref Expression
pwrssmgc (πœ‘ β†’ 𝐺(𝑉MGalConnπ‘Š)𝐻)
Distinct variable groups:   π‘š,𝐹,𝑦   𝑛,𝐹   π‘š,𝑉,𝑦   𝑛,𝑉   π‘š,π‘Š,𝑦   𝑛,π‘Š   π‘š,𝑋   𝑛,𝑋   π‘š,π‘Œ,𝑦   𝑛,π‘Œ   πœ‘,𝑦,π‘š   πœ‘,𝑛
Allowed substitution hints:   𝐴(𝑦,π‘š,𝑛)   𝐡(𝑦,π‘š,𝑛)   𝐺(𝑦,π‘š,𝑛)   𝐻(𝑦,π‘š,𝑛)   𝑋(𝑦)

Proof of Theorem pwrssmgc
Dummy variables 𝑖 𝑗 𝑒 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pwrssmgc.5 . . . . . . 7 (πœ‘ β†’ 𝑋 ∈ 𝐴)
21adantr 482 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ 𝒫 π‘Œ) β†’ 𝑋 ∈ 𝐴)
3 cnvimass 6038 . . . . . . . 8 (◑𝐹 β€œ 𝑛) βŠ† dom 𝐹
4 pwrssmgc.7 . . . . . . . 8 (πœ‘ β†’ 𝐹:π‘‹βŸΆπ‘Œ)
53, 4fssdm 6693 . . . . . . 7 (πœ‘ β†’ (◑𝐹 β€œ 𝑛) βŠ† 𝑋)
65adantr 482 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ 𝒫 π‘Œ) β†’ (◑𝐹 β€œ 𝑛) βŠ† 𝑋)
72, 6sselpwd 5288 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ 𝒫 π‘Œ) β†’ (◑𝐹 β€œ 𝑛) ∈ 𝒫 𝑋)
8 pwrssmgc.1 . . . . 5 𝐺 = (𝑛 ∈ 𝒫 π‘Œ ↦ (◑𝐹 β€œ 𝑛))
97, 8fmptd 7067 . . . 4 (πœ‘ β†’ 𝐺:𝒫 π‘ŒβŸΆπ’« 𝑋)
10 pwrssmgc.6 . . . . . 6 (πœ‘ β†’ π‘Œ ∈ 𝐡)
11 pwexg 5338 . . . . . 6 (π‘Œ ∈ 𝐡 β†’ 𝒫 π‘Œ ∈ V)
12 pwrssmgc.3 . . . . . . 7 𝑉 = (toIncβ€˜π’« π‘Œ)
1312ipobas 18427 . . . . . 6 (𝒫 π‘Œ ∈ V β†’ 𝒫 π‘Œ = (Baseβ€˜π‘‰))
1410, 11, 133syl 18 . . . . 5 (πœ‘ β†’ 𝒫 π‘Œ = (Baseβ€˜π‘‰))
15 pwexg 5338 . . . . . 6 (𝑋 ∈ 𝐴 β†’ 𝒫 𝑋 ∈ V)
16 pwrssmgc.4 . . . . . . 7 π‘Š = (toIncβ€˜π’« 𝑋)
1716ipobas 18427 . . . . . 6 (𝒫 𝑋 ∈ V β†’ 𝒫 𝑋 = (Baseβ€˜π‘Š))
181, 15, 173syl 18 . . . . 5 (πœ‘ β†’ 𝒫 𝑋 = (Baseβ€˜π‘Š))
1914, 18feq23d 6668 . . . 4 (πœ‘ β†’ (𝐺:𝒫 π‘ŒβŸΆπ’« 𝑋 ↔ 𝐺:(Baseβ€˜π‘‰)⟢(Baseβ€˜π‘Š)))
209, 19mpbid 231 . . 3 (πœ‘ β†’ 𝐺:(Baseβ€˜π‘‰)⟢(Baseβ€˜π‘Š))
2110adantr 482 . . . . . 6 ((πœ‘ ∧ π‘š ∈ 𝒫 𝑋) β†’ π‘Œ ∈ 𝐡)
22 ssrab2 4042 . . . . . . 7 {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† π‘š} βŠ† π‘Œ
2322a1i 11 . . . . . 6 ((πœ‘ ∧ π‘š ∈ 𝒫 𝑋) β†’ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† π‘š} βŠ† π‘Œ)
2421, 23sselpwd 5288 . . . . 5 ((πœ‘ ∧ π‘š ∈ 𝒫 𝑋) β†’ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† π‘š} ∈ 𝒫 π‘Œ)
25 pwrssmgc.2 . . . . 5 𝐻 = (π‘š ∈ 𝒫 𝑋 ↦ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† π‘š})
2624, 25fmptd 7067 . . . 4 (πœ‘ β†’ 𝐻:𝒫 π‘‹βŸΆπ’« π‘Œ)
2718, 14feq23d 6668 . . . 4 (πœ‘ β†’ (𝐻:𝒫 π‘‹βŸΆπ’« π‘Œ ↔ 𝐻:(Baseβ€˜π‘Š)⟢(Baseβ€˜π‘‰)))
2826, 27mpbid 231 . . 3 (πœ‘ β†’ 𝐻:(Baseβ€˜π‘Š)⟢(Baseβ€˜π‘‰))
2920, 28jca 513 . 2 (πœ‘ β†’ (𝐺:(Baseβ€˜π‘‰)⟢(Baseβ€˜π‘Š) ∧ 𝐻:(Baseβ€˜π‘Š)⟢(Baseβ€˜π‘‰)))
30 sneq 4601 . . . . . . . . . . . 12 (𝑦 = 𝑗 β†’ {𝑦} = {𝑗})
3130imaeq2d 6018 . . . . . . . . . . 11 (𝑦 = 𝑗 β†’ (◑𝐹 β€œ {𝑦}) = (◑𝐹 β€œ {𝑗}))
3231sseq1d 3980 . . . . . . . . . 10 (𝑦 = 𝑗 β†’ ((◑𝐹 β€œ {𝑦}) βŠ† 𝑣 ↔ (◑𝐹 β€œ {𝑗}) βŠ† 𝑣))
33 simplr 768 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ 𝑒 ∈ (Baseβ€˜π‘‰))
3414ad2antrr 725 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ 𝒫 π‘Œ = (Baseβ€˜π‘‰))
3533, 34eleqtrrd 2841 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ 𝑒 ∈ 𝒫 π‘Œ)
3635adantr 482 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ (◑𝐹 β€œ 𝑒) βŠ† 𝑣) β†’ 𝑒 ∈ 𝒫 π‘Œ)
3736elpwid 4574 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ (◑𝐹 β€œ 𝑒) βŠ† 𝑣) β†’ 𝑒 βŠ† π‘Œ)
3837sselda 3949 . . . . . . . . . 10 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ (◑𝐹 β€œ 𝑒) βŠ† 𝑣) ∧ 𝑗 ∈ 𝑒) β†’ 𝑗 ∈ π‘Œ)
394ffund 6677 . . . . . . . . . . . . 13 (πœ‘ β†’ Fun 𝐹)
4039ad4antr 731 . . . . . . . . . . . 12 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ (◑𝐹 β€œ 𝑒) βŠ† 𝑣) ∧ 𝑗 ∈ 𝑒) β†’ Fun 𝐹)
41 snssi 4773 . . . . . . . . . . . . 13 (𝑗 ∈ 𝑒 β†’ {𝑗} βŠ† 𝑒)
4241adantl 483 . . . . . . . . . . . 12 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ (◑𝐹 β€œ 𝑒) βŠ† 𝑣) ∧ 𝑗 ∈ 𝑒) β†’ {𝑗} βŠ† 𝑒)
43 sspreima 7023 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ {𝑗} βŠ† 𝑒) β†’ (◑𝐹 β€œ {𝑗}) βŠ† (◑𝐹 β€œ 𝑒))
4440, 42, 43syl2anc 585 . . . . . . . . . . 11 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ (◑𝐹 β€œ 𝑒) βŠ† 𝑣) ∧ 𝑗 ∈ 𝑒) β†’ (◑𝐹 β€œ {𝑗}) βŠ† (◑𝐹 β€œ 𝑒))
45 simplr 768 . . . . . . . . . . 11 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ (◑𝐹 β€œ 𝑒) βŠ† 𝑣) ∧ 𝑗 ∈ 𝑒) β†’ (◑𝐹 β€œ 𝑒) βŠ† 𝑣)
4644, 45sstrd 3959 . . . . . . . . . 10 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ (◑𝐹 β€œ 𝑒) βŠ† 𝑣) ∧ 𝑗 ∈ 𝑒) β†’ (◑𝐹 β€œ {𝑗}) βŠ† 𝑣)
4732, 38, 46elrabd 3652 . . . . . . . . 9 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ (◑𝐹 β€œ 𝑒) βŠ† 𝑣) ∧ 𝑗 ∈ 𝑒) β†’ 𝑗 ∈ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣})
4847ex 414 . . . . . . . 8 ((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ (◑𝐹 β€œ 𝑒) βŠ† 𝑣) β†’ (𝑗 ∈ 𝑒 β†’ 𝑗 ∈ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}))
4948ssrdv 3955 . . . . . . 7 ((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ (◑𝐹 β€œ 𝑒) βŠ† 𝑣) β†’ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣})
50 simplr 768 . . . . . . . . . . . 12 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣})
514ffnd 6674 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐹 Fn 𝑋)
5251ad4antr 731 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ 𝐹 Fn 𝑋)
53 simpr 486 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ 𝑖 ∈ (◑𝐹 β€œ 𝑒))
54 elpreima 7013 . . . . . . . . . . . . . . 15 (𝐹 Fn 𝑋 β†’ (𝑖 ∈ (◑𝐹 β€œ 𝑒) ↔ (𝑖 ∈ 𝑋 ∧ (πΉβ€˜π‘–) ∈ 𝑒)))
5554biimpa 478 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝑋 ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ (𝑖 ∈ 𝑋 ∧ (πΉβ€˜π‘–) ∈ 𝑒))
5652, 53, 55syl2anc 585 . . . . . . . . . . . . 13 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ (𝑖 ∈ 𝑋 ∧ (πΉβ€˜π‘–) ∈ 𝑒))
5756simprd 497 . . . . . . . . . . . 12 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ (πΉβ€˜π‘–) ∈ 𝑒)
5850, 57sseldd 3950 . . . . . . . . . . 11 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ (πΉβ€˜π‘–) ∈ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣})
59 sneq 4601 . . . . . . . . . . . . . . 15 (𝑦 = (πΉβ€˜π‘–) β†’ {𝑦} = {(πΉβ€˜π‘–)})
6059imaeq2d 6018 . . . . . . . . . . . . . 14 (𝑦 = (πΉβ€˜π‘–) β†’ (◑𝐹 β€œ {𝑦}) = (◑𝐹 β€œ {(πΉβ€˜π‘–)}))
6160sseq1d 3980 . . . . . . . . . . . . 13 (𝑦 = (πΉβ€˜π‘–) β†’ ((◑𝐹 β€œ {𝑦}) βŠ† 𝑣 ↔ (◑𝐹 β€œ {(πΉβ€˜π‘–)}) βŠ† 𝑣))
6261elrab 3650 . . . . . . . . . . . 12 ((πΉβ€˜π‘–) ∈ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣} ↔ ((πΉβ€˜π‘–) ∈ π‘Œ ∧ (◑𝐹 β€œ {(πΉβ€˜π‘–)}) βŠ† 𝑣))
6362simprbi 498 . . . . . . . . . . 11 ((πΉβ€˜π‘–) ∈ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣} β†’ (◑𝐹 β€œ {(πΉβ€˜π‘–)}) βŠ† 𝑣)
6458, 63syl 17 . . . . . . . . . 10 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ (◑𝐹 β€œ {(πΉβ€˜π‘–)}) βŠ† 𝑣)
6556simpld 496 . . . . . . . . . . 11 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ 𝑖 ∈ 𝑋)
66 eqidd 2738 . . . . . . . . . . 11 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ (πΉβ€˜π‘–) = (πΉβ€˜π‘–))
67 fniniseg 7015 . . . . . . . . . . . 12 (𝐹 Fn 𝑋 β†’ (𝑖 ∈ (◑𝐹 β€œ {(πΉβ€˜π‘–)}) ↔ (𝑖 ∈ 𝑋 ∧ (πΉβ€˜π‘–) = (πΉβ€˜π‘–))))
6867biimpar 479 . . . . . . . . . . 11 ((𝐹 Fn 𝑋 ∧ (𝑖 ∈ 𝑋 ∧ (πΉβ€˜π‘–) = (πΉβ€˜π‘–))) β†’ 𝑖 ∈ (◑𝐹 β€œ {(πΉβ€˜π‘–)}))
6952, 65, 66, 68syl12anc 836 . . . . . . . . . 10 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ 𝑖 ∈ (◑𝐹 β€œ {(πΉβ€˜π‘–)}))
7064, 69sseldd 3950 . . . . . . . . 9 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ 𝑖 ∈ 𝑣)
7170ex 414 . . . . . . . 8 ((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) β†’ (𝑖 ∈ (◑𝐹 β€œ 𝑒) β†’ 𝑖 ∈ 𝑣))
7271ssrdv 3955 . . . . . . 7 ((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) β†’ (◑𝐹 β€œ 𝑒) βŠ† 𝑣)
7349, 72impbida 800 . . . . . 6 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ ((◑𝐹 β€œ 𝑒) βŠ† 𝑣 ↔ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}))
74 simpr 486 . . . . . . . . 9 ((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑛 = 𝑒) β†’ 𝑛 = 𝑒)
7574imaeq2d 6018 . . . . . . . 8 ((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑛 = 𝑒) β†’ (◑𝐹 β€œ 𝑛) = (◑𝐹 β€œ 𝑒))
764, 1fexd 7182 . . . . . . . . . 10 (πœ‘ β†’ 𝐹 ∈ V)
77 cnvexg 7866 . . . . . . . . . 10 (𝐹 ∈ V β†’ ◑𝐹 ∈ V)
78 imaexg 7857 . . . . . . . . . 10 (◑𝐹 ∈ V β†’ (◑𝐹 β€œ 𝑒) ∈ V)
7976, 77, 783syl 18 . . . . . . . . 9 (πœ‘ β†’ (◑𝐹 β€œ 𝑒) ∈ V)
8079ad2antrr 725 . . . . . . . 8 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ (◑𝐹 β€œ 𝑒) ∈ V)
818, 75, 35, 80fvmptd2 6961 . . . . . . 7 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ (πΊβ€˜π‘’) = (◑𝐹 β€œ 𝑒))
8281sseq1d 3980 . . . . . 6 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ ((πΊβ€˜π‘’) βŠ† 𝑣 ↔ (◑𝐹 β€œ 𝑒) βŠ† 𝑣))
83 simpr 486 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ π‘š = 𝑣) β†’ π‘š = 𝑣)
8483sseq2d 3981 . . . . . . . . 9 ((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ π‘š = 𝑣) β†’ ((◑𝐹 β€œ {𝑦}) βŠ† π‘š ↔ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣))
8584rabbidv 3418 . . . . . . . 8 ((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ π‘š = 𝑣) β†’ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† π‘š} = {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣})
86 simpr 486 . . . . . . . . 9 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ 𝑣 ∈ (Baseβ€˜π‘Š))
871, 15syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 𝒫 𝑋 ∈ V)
8887ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ 𝒫 𝑋 ∈ V)
8988, 17syl 17 . . . . . . . . 9 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ 𝒫 𝑋 = (Baseβ€˜π‘Š))
9086, 89eleqtrrd 2841 . . . . . . . 8 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ 𝑣 ∈ 𝒫 𝑋)
9110ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ π‘Œ ∈ 𝐡)
92 ssrab2 4042 . . . . . . . . . 10 {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣} βŠ† π‘Œ
9392a1i 11 . . . . . . . . 9 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣} βŠ† π‘Œ)
9491, 93sselpwd 5288 . . . . . . . 8 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣} ∈ 𝒫 π‘Œ)
9525, 85, 90, 94fvmptd2 6961 . . . . . . 7 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ (π»β€˜π‘£) = {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣})
9695sseq2d 3981 . . . . . 6 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ (𝑒 βŠ† (π»β€˜π‘£) ↔ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}))
9773, 82, 963bitr4d 311 . . . . 5 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ ((πΊβ€˜π‘’) βŠ† 𝑣 ↔ 𝑒 βŠ† (π»β€˜π‘£)))
989ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ 𝐺:𝒫 π‘ŒβŸΆπ’« 𝑋)
9998, 35ffvelcdmd 7041 . . . . . 6 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ (πΊβ€˜π‘’) ∈ 𝒫 𝑋)
100 eqid 2737 . . . . . . 7 (leβ€˜π‘Š) = (leβ€˜π‘Š)
10116, 100ipole 18430 . . . . . 6 ((𝒫 𝑋 ∈ V ∧ (πΊβ€˜π‘’) ∈ 𝒫 𝑋 ∧ 𝑣 ∈ 𝒫 𝑋) β†’ ((πΊβ€˜π‘’)(leβ€˜π‘Š)𝑣 ↔ (πΊβ€˜π‘’) βŠ† 𝑣))
10288, 99, 90, 101syl3anc 1372 . . . . 5 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ ((πΊβ€˜π‘’)(leβ€˜π‘Š)𝑣 ↔ (πΊβ€˜π‘’) βŠ† 𝑣))
10310, 11syl 17 . . . . . . 7 (πœ‘ β†’ 𝒫 π‘Œ ∈ V)
104103ad2antrr 725 . . . . . 6 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ 𝒫 π‘Œ ∈ V)
10526ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ 𝐻:𝒫 π‘‹βŸΆπ’« π‘Œ)
106105, 90ffvelcdmd 7041 . . . . . 6 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ (π»β€˜π‘£) ∈ 𝒫 π‘Œ)
107 eqid 2737 . . . . . . 7 (leβ€˜π‘‰) = (leβ€˜π‘‰)
10812, 107ipole 18430 . . . . . 6 ((𝒫 π‘Œ ∈ V ∧ 𝑒 ∈ 𝒫 π‘Œ ∧ (π»β€˜π‘£) ∈ 𝒫 π‘Œ) β†’ (𝑒(leβ€˜π‘‰)(π»β€˜π‘£) ↔ 𝑒 βŠ† (π»β€˜π‘£)))
109104, 35, 106, 108syl3anc 1372 . . . . 5 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ (𝑒(leβ€˜π‘‰)(π»β€˜π‘£) ↔ 𝑒 βŠ† (π»β€˜π‘£)))
11097, 102, 1093bitr4d 311 . . . 4 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ ((πΊβ€˜π‘’)(leβ€˜π‘Š)𝑣 ↔ 𝑒(leβ€˜π‘‰)(π»β€˜π‘£)))
111110anasss 468 . . 3 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘‰) ∧ 𝑣 ∈ (Baseβ€˜π‘Š))) β†’ ((πΊβ€˜π‘’)(leβ€˜π‘Š)𝑣 ↔ 𝑒(leβ€˜π‘‰)(π»β€˜π‘£)))
112111ralrimivva 3198 . 2 (πœ‘ β†’ βˆ€π‘’ ∈ (Baseβ€˜π‘‰)βˆ€π‘£ ∈ (Baseβ€˜π‘Š)((πΊβ€˜π‘’)(leβ€˜π‘Š)𝑣 ↔ 𝑒(leβ€˜π‘‰)(π»β€˜π‘£)))
113 eqid 2737 . . 3 (Baseβ€˜π‘‰) = (Baseβ€˜π‘‰)
114 eqid 2737 . . 3 (Baseβ€˜π‘Š) = (Baseβ€˜π‘Š)
115 eqid 2737 . . 3 (𝑉MGalConnπ‘Š) = (𝑉MGalConnπ‘Š)
11612ipopos 18432 . . . 4 𝑉 ∈ Poset
117 posprs 18212 . . . 4 (𝑉 ∈ Poset β†’ 𝑉 ∈ Proset )
118116, 117mp1i 13 . . 3 (πœ‘ β†’ 𝑉 ∈ Proset )
11916ipopos 18432 . . . 4 π‘Š ∈ Poset
120 posprs 18212 . . . 4 (π‘Š ∈ Poset β†’ π‘Š ∈ Proset )
121119, 120mp1i 13 . . 3 (πœ‘ β†’ π‘Š ∈ Proset )
122113, 114, 107, 100, 115, 118, 121mgcval 31889 . 2 (πœ‘ β†’ (𝐺(𝑉MGalConnπ‘Š)𝐻 ↔ ((𝐺:(Baseβ€˜π‘‰)⟢(Baseβ€˜π‘Š) ∧ 𝐻:(Baseβ€˜π‘Š)⟢(Baseβ€˜π‘‰)) ∧ βˆ€π‘’ ∈ (Baseβ€˜π‘‰)βˆ€π‘£ ∈ (Baseβ€˜π‘Š)((πΊβ€˜π‘’)(leβ€˜π‘Š)𝑣 ↔ 𝑒(leβ€˜π‘‰)(π»β€˜π‘£)))))
12329, 112, 122mpbir2and 712 1 (πœ‘ β†’ 𝐺(𝑉MGalConnπ‘Š)𝐻)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βˆ€wral 3065  {crab 3410  Vcvv 3448   βŠ† wss 3915  π’« cpw 4565  {csn 4591   class class class wbr 5110   ↦ cmpt 5193  β—‘ccnv 5637   β€œ cima 5641  Fun wfun 6495   Fn wfn 6496  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362  Basecbs 17090  lecple 17147   Proset cproset 18189  Posetcpo 18203  toInccipo 18423  MGalConncmgc 31881
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 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-map 8774  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-z 12507  df-dec 12626  df-uz 12771  df-fz 13432  df-struct 17026  df-slot 17061  df-ndx 17073  df-base 17091  df-tset 17159  df-ple 17160  df-ocomp 17161  df-proset 18191  df-poset 18209  df-ipo 18424  df-mgc 31883
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator