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 32208
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 481 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ 𝒫 π‘Œ) β†’ 𝑋 ∈ 𝐴)
3 cnvimass 6080 . . . . . . . 8 (◑𝐹 β€œ 𝑛) βŠ† dom 𝐹
4 pwrssmgc.7 . . . . . . . 8 (πœ‘ β†’ 𝐹:π‘‹βŸΆπ‘Œ)
53, 4fssdm 6737 . . . . . . 7 (πœ‘ β†’ (◑𝐹 β€œ 𝑛) βŠ† 𝑋)
65adantr 481 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ 𝒫 π‘Œ) β†’ (◑𝐹 β€œ 𝑛) βŠ† 𝑋)
72, 6sselpwd 5326 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ 𝒫 π‘Œ) β†’ (◑𝐹 β€œ 𝑛) ∈ 𝒫 𝑋)
8 pwrssmgc.1 . . . . 5 𝐺 = (𝑛 ∈ 𝒫 π‘Œ ↦ (◑𝐹 β€œ 𝑛))
97, 8fmptd 7115 . . . 4 (πœ‘ β†’ 𝐺:𝒫 π‘ŒβŸΆπ’« 𝑋)
10 pwrssmgc.6 . . . . . 6 (πœ‘ β†’ π‘Œ ∈ 𝐡)
11 pwexg 5376 . . . . . 6 (π‘Œ ∈ 𝐡 β†’ 𝒫 π‘Œ ∈ V)
12 pwrssmgc.3 . . . . . . 7 𝑉 = (toIncβ€˜π’« π‘Œ)
1312ipobas 18486 . . . . . 6 (𝒫 π‘Œ ∈ V β†’ 𝒫 π‘Œ = (Baseβ€˜π‘‰))
1410, 11, 133syl 18 . . . . 5 (πœ‘ β†’ 𝒫 π‘Œ = (Baseβ€˜π‘‰))
15 pwexg 5376 . . . . . 6 (𝑋 ∈ 𝐴 β†’ 𝒫 𝑋 ∈ V)
16 pwrssmgc.4 . . . . . . 7 π‘Š = (toIncβ€˜π’« 𝑋)
1716ipobas 18486 . . . . . 6 (𝒫 𝑋 ∈ V β†’ 𝒫 𝑋 = (Baseβ€˜π‘Š))
181, 15, 173syl 18 . . . . 5 (πœ‘ β†’ 𝒫 𝑋 = (Baseβ€˜π‘Š))
1914, 18feq23d 6712 . . . 4 (πœ‘ β†’ (𝐺:𝒫 π‘ŒβŸΆπ’« 𝑋 ↔ 𝐺:(Baseβ€˜π‘‰)⟢(Baseβ€˜π‘Š)))
209, 19mpbid 231 . . 3 (πœ‘ β†’ 𝐺:(Baseβ€˜π‘‰)⟢(Baseβ€˜π‘Š))
2110adantr 481 . . . . . 6 ((πœ‘ ∧ π‘š ∈ 𝒫 𝑋) β†’ π‘Œ ∈ 𝐡)
22 ssrab2 4077 . . . . . . 7 {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† π‘š} βŠ† π‘Œ
2322a1i 11 . . . . . 6 ((πœ‘ ∧ π‘š ∈ 𝒫 𝑋) β†’ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† π‘š} βŠ† π‘Œ)
2421, 23sselpwd 5326 . . . . 5 ((πœ‘ ∧ π‘š ∈ 𝒫 𝑋) β†’ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† π‘š} ∈ 𝒫 π‘Œ)
25 pwrssmgc.2 . . . . 5 𝐻 = (π‘š ∈ 𝒫 𝑋 ↦ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† π‘š})
2624, 25fmptd 7115 . . . 4 (πœ‘ β†’ 𝐻:𝒫 π‘‹βŸΆπ’« π‘Œ)
2718, 14feq23d 6712 . . . 4 (πœ‘ β†’ (𝐻:𝒫 π‘‹βŸΆπ’« π‘Œ ↔ 𝐻:(Baseβ€˜π‘Š)⟢(Baseβ€˜π‘‰)))
2826, 27mpbid 231 . . 3 (πœ‘ β†’ 𝐻:(Baseβ€˜π‘Š)⟢(Baseβ€˜π‘‰))
2920, 28jca 512 . 2 (πœ‘ β†’ (𝐺:(Baseβ€˜π‘‰)⟢(Baseβ€˜π‘Š) ∧ 𝐻:(Baseβ€˜π‘Š)⟢(Baseβ€˜π‘‰)))
30 sneq 4638 . . . . . . . . . . . 12 (𝑦 = 𝑗 β†’ {𝑦} = {𝑗})
3130imaeq2d 6059 . . . . . . . . . . 11 (𝑦 = 𝑗 β†’ (◑𝐹 β€œ {𝑦}) = (◑𝐹 β€œ {𝑗}))
3231sseq1d 4013 . . . . . . . . . 10 (𝑦 = 𝑗 β†’ ((◑𝐹 β€œ {𝑦}) βŠ† 𝑣 ↔ (◑𝐹 β€œ {𝑗}) βŠ† 𝑣))
33 simplr 767 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ 𝑒 ∈ (Baseβ€˜π‘‰))
3414ad2antrr 724 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ 𝒫 π‘Œ = (Baseβ€˜π‘‰))
3533, 34eleqtrrd 2836 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ 𝑒 ∈ 𝒫 π‘Œ)
3635adantr 481 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ (◑𝐹 β€œ 𝑒) βŠ† 𝑣) β†’ 𝑒 ∈ 𝒫 π‘Œ)
3736elpwid 4611 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ (◑𝐹 β€œ 𝑒) βŠ† 𝑣) β†’ 𝑒 βŠ† π‘Œ)
3837sselda 3982 . . . . . . . . . 10 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ (◑𝐹 β€œ 𝑒) βŠ† 𝑣) ∧ 𝑗 ∈ 𝑒) β†’ 𝑗 ∈ π‘Œ)
394ffund 6721 . . . . . . . . . . . . 13 (πœ‘ β†’ Fun 𝐹)
4039ad4antr 730 . . . . . . . . . . . 12 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ (◑𝐹 β€œ 𝑒) βŠ† 𝑣) ∧ 𝑗 ∈ 𝑒) β†’ Fun 𝐹)
41 snssi 4811 . . . . . . . . . . . . 13 (𝑗 ∈ 𝑒 β†’ {𝑗} βŠ† 𝑒)
4241adantl 482 . . . . . . . . . . . 12 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ (◑𝐹 β€œ 𝑒) βŠ† 𝑣) ∧ 𝑗 ∈ 𝑒) β†’ {𝑗} βŠ† 𝑒)
43 sspreima 7069 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ {𝑗} βŠ† 𝑒) β†’ (◑𝐹 β€œ {𝑗}) βŠ† (◑𝐹 β€œ 𝑒))
4440, 42, 43syl2anc 584 . . . . . . . . . . 11 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ (◑𝐹 β€œ 𝑒) βŠ† 𝑣) ∧ 𝑗 ∈ 𝑒) β†’ (◑𝐹 β€œ {𝑗}) βŠ† (◑𝐹 β€œ 𝑒))
45 simplr 767 . . . . . . . . . . 11 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ (◑𝐹 β€œ 𝑒) βŠ† 𝑣) ∧ 𝑗 ∈ 𝑒) β†’ (◑𝐹 β€œ 𝑒) βŠ† 𝑣)
4644, 45sstrd 3992 . . . . . . . . . 10 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ (◑𝐹 β€œ 𝑒) βŠ† 𝑣) ∧ 𝑗 ∈ 𝑒) β†’ (◑𝐹 β€œ {𝑗}) βŠ† 𝑣)
4732, 38, 46elrabd 3685 . . . . . . . . 9 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ (◑𝐹 β€œ 𝑒) βŠ† 𝑣) ∧ 𝑗 ∈ 𝑒) β†’ 𝑗 ∈ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣})
4847ex 413 . . . . . . . 8 ((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ (◑𝐹 β€œ 𝑒) βŠ† 𝑣) β†’ (𝑗 ∈ 𝑒 β†’ 𝑗 ∈ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}))
4948ssrdv 3988 . . . . . . 7 ((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ (◑𝐹 β€œ 𝑒) βŠ† 𝑣) β†’ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣})
50 simplr 767 . . . . . . . . . . . 12 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣})
514ffnd 6718 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐹 Fn 𝑋)
5251ad4antr 730 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ 𝐹 Fn 𝑋)
53 simpr 485 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ 𝑖 ∈ (◑𝐹 β€œ 𝑒))
54 elpreima 7059 . . . . . . . . . . . . . . 15 (𝐹 Fn 𝑋 β†’ (𝑖 ∈ (◑𝐹 β€œ 𝑒) ↔ (𝑖 ∈ 𝑋 ∧ (πΉβ€˜π‘–) ∈ 𝑒)))
5554biimpa 477 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝑋 ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ (𝑖 ∈ 𝑋 ∧ (πΉβ€˜π‘–) ∈ 𝑒))
5652, 53, 55syl2anc 584 . . . . . . . . . . . . 13 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ (𝑖 ∈ 𝑋 ∧ (πΉβ€˜π‘–) ∈ 𝑒))
5756simprd 496 . . . . . . . . . . . 12 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ (πΉβ€˜π‘–) ∈ 𝑒)
5850, 57sseldd 3983 . . . . . . . . . . 11 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ (πΉβ€˜π‘–) ∈ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣})
59 sneq 4638 . . . . . . . . . . . . . . 15 (𝑦 = (πΉβ€˜π‘–) β†’ {𝑦} = {(πΉβ€˜π‘–)})
6059imaeq2d 6059 . . . . . . . . . . . . . 14 (𝑦 = (πΉβ€˜π‘–) β†’ (◑𝐹 β€œ {𝑦}) = (◑𝐹 β€œ {(πΉβ€˜π‘–)}))
6160sseq1d 4013 . . . . . . . . . . . . 13 (𝑦 = (πΉβ€˜π‘–) β†’ ((◑𝐹 β€œ {𝑦}) βŠ† 𝑣 ↔ (◑𝐹 β€œ {(πΉβ€˜π‘–)}) βŠ† 𝑣))
6261elrab 3683 . . . . . . . . . . . 12 ((πΉβ€˜π‘–) ∈ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣} ↔ ((πΉβ€˜π‘–) ∈ π‘Œ ∧ (◑𝐹 β€œ {(πΉβ€˜π‘–)}) βŠ† 𝑣))
6362simprbi 497 . . . . . . . . . . 11 ((πΉβ€˜π‘–) ∈ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣} β†’ (◑𝐹 β€œ {(πΉβ€˜π‘–)}) βŠ† 𝑣)
6458, 63syl 17 . . . . . . . . . 10 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ (◑𝐹 β€œ {(πΉβ€˜π‘–)}) βŠ† 𝑣)
6556simpld 495 . . . . . . . . . . 11 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ 𝑖 ∈ 𝑋)
66 eqidd 2733 . . . . . . . . . . 11 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ (πΉβ€˜π‘–) = (πΉβ€˜π‘–))
67 fniniseg 7061 . . . . . . . . . . . 12 (𝐹 Fn 𝑋 β†’ (𝑖 ∈ (◑𝐹 β€œ {(πΉβ€˜π‘–)}) ↔ (𝑖 ∈ 𝑋 ∧ (πΉβ€˜π‘–) = (πΉβ€˜π‘–))))
6867biimpar 478 . . . . . . . . . . 11 ((𝐹 Fn 𝑋 ∧ (𝑖 ∈ 𝑋 ∧ (πΉβ€˜π‘–) = (πΉβ€˜π‘–))) β†’ 𝑖 ∈ (◑𝐹 β€œ {(πΉβ€˜π‘–)}))
6952, 65, 66, 68syl12anc 835 . . . . . . . . . 10 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ 𝑖 ∈ (◑𝐹 β€œ {(πΉβ€˜π‘–)}))
7064, 69sseldd 3983 . . . . . . . . 9 (((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) ∧ 𝑖 ∈ (◑𝐹 β€œ 𝑒)) β†’ 𝑖 ∈ 𝑣)
7170ex 413 . . . . . . . 8 ((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) β†’ (𝑖 ∈ (◑𝐹 β€œ 𝑒) β†’ 𝑖 ∈ 𝑣))
7271ssrdv 3988 . . . . . . 7 ((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}) β†’ (◑𝐹 β€œ 𝑒) βŠ† 𝑣)
7349, 72impbida 799 . . . . . 6 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ ((◑𝐹 β€œ 𝑒) βŠ† 𝑣 ↔ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}))
74 simpr 485 . . . . . . . . 9 ((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑛 = 𝑒) β†’ 𝑛 = 𝑒)
7574imaeq2d 6059 . . . . . . . 8 ((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ 𝑛 = 𝑒) β†’ (◑𝐹 β€œ 𝑛) = (◑𝐹 β€œ 𝑒))
764, 1fexd 7231 . . . . . . . . . 10 (πœ‘ β†’ 𝐹 ∈ V)
77 cnvexg 7917 . . . . . . . . . 10 (𝐹 ∈ V β†’ ◑𝐹 ∈ V)
78 imaexg 7908 . . . . . . . . . 10 (◑𝐹 ∈ V β†’ (◑𝐹 β€œ 𝑒) ∈ V)
7976, 77, 783syl 18 . . . . . . . . 9 (πœ‘ β†’ (◑𝐹 β€œ 𝑒) ∈ V)
8079ad2antrr 724 . . . . . . . 8 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ (◑𝐹 β€œ 𝑒) ∈ V)
818, 75, 35, 80fvmptd2 7006 . . . . . . 7 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ (πΊβ€˜π‘’) = (◑𝐹 β€œ 𝑒))
8281sseq1d 4013 . . . . . 6 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ ((πΊβ€˜π‘’) βŠ† 𝑣 ↔ (◑𝐹 β€œ 𝑒) βŠ† 𝑣))
83 simpr 485 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ π‘š = 𝑣) β†’ π‘š = 𝑣)
8483sseq2d 4014 . . . . . . . . 9 ((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ π‘š = 𝑣) β†’ ((◑𝐹 β€œ {𝑦}) βŠ† π‘š ↔ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣))
8584rabbidv 3440 . . . . . . . 8 ((((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) ∧ π‘š = 𝑣) β†’ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† π‘š} = {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣})
86 simpr 485 . . . . . . . . 9 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ 𝑣 ∈ (Baseβ€˜π‘Š))
871, 15syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 𝒫 𝑋 ∈ V)
8887ad2antrr 724 . . . . . . . . . 10 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ 𝒫 𝑋 ∈ V)
8988, 17syl 17 . . . . . . . . 9 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ 𝒫 𝑋 = (Baseβ€˜π‘Š))
9086, 89eleqtrrd 2836 . . . . . . . 8 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ 𝑣 ∈ 𝒫 𝑋)
9110ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ π‘Œ ∈ 𝐡)
92 ssrab2 4077 . . . . . . . . . 10 {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣} βŠ† π‘Œ
9392a1i 11 . . . . . . . . 9 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣} βŠ† π‘Œ)
9491, 93sselpwd 5326 . . . . . . . 8 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣} ∈ 𝒫 π‘Œ)
9525, 85, 90, 94fvmptd2 7006 . . . . . . 7 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ (π»β€˜π‘£) = {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣})
9695sseq2d 4014 . . . . . 6 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ (𝑒 βŠ† (π»β€˜π‘£) ↔ 𝑒 βŠ† {𝑦 ∈ π‘Œ ∣ (◑𝐹 β€œ {𝑦}) βŠ† 𝑣}))
9773, 82, 963bitr4d 310 . . . . 5 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ ((πΊβ€˜π‘’) βŠ† 𝑣 ↔ 𝑒 βŠ† (π»β€˜π‘£)))
989ad2antrr 724 . . . . . . 7 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ 𝐺:𝒫 π‘ŒβŸΆπ’« 𝑋)
9998, 35ffvelcdmd 7087 . . . . . 6 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ (πΊβ€˜π‘’) ∈ 𝒫 𝑋)
100 eqid 2732 . . . . . . 7 (leβ€˜π‘Š) = (leβ€˜π‘Š)
10116, 100ipole 18489 . . . . . 6 ((𝒫 𝑋 ∈ V ∧ (πΊβ€˜π‘’) ∈ 𝒫 𝑋 ∧ 𝑣 ∈ 𝒫 𝑋) β†’ ((πΊβ€˜π‘’)(leβ€˜π‘Š)𝑣 ↔ (πΊβ€˜π‘’) βŠ† 𝑣))
10288, 99, 90, 101syl3anc 1371 . . . . 5 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ ((πΊβ€˜π‘’)(leβ€˜π‘Š)𝑣 ↔ (πΊβ€˜π‘’) βŠ† 𝑣))
10310, 11syl 17 . . . . . . 7 (πœ‘ β†’ 𝒫 π‘Œ ∈ V)
104103ad2antrr 724 . . . . . 6 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ 𝒫 π‘Œ ∈ V)
10526ad2antrr 724 . . . . . . 7 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ 𝐻:𝒫 π‘‹βŸΆπ’« π‘Œ)
106105, 90ffvelcdmd 7087 . . . . . 6 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ (π»β€˜π‘£) ∈ 𝒫 π‘Œ)
107 eqid 2732 . . . . . . 7 (leβ€˜π‘‰) = (leβ€˜π‘‰)
10812, 107ipole 18489 . . . . . 6 ((𝒫 π‘Œ ∈ V ∧ 𝑒 ∈ 𝒫 π‘Œ ∧ (π»β€˜π‘£) ∈ 𝒫 π‘Œ) β†’ (𝑒(leβ€˜π‘‰)(π»β€˜π‘£) ↔ 𝑒 βŠ† (π»β€˜π‘£)))
109104, 35, 106, 108syl3anc 1371 . . . . 5 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ (𝑒(leβ€˜π‘‰)(π»β€˜π‘£) ↔ 𝑒 βŠ† (π»β€˜π‘£)))
11097, 102, 1093bitr4d 310 . . . 4 (((πœ‘ ∧ 𝑒 ∈ (Baseβ€˜π‘‰)) ∧ 𝑣 ∈ (Baseβ€˜π‘Š)) β†’ ((πΊβ€˜π‘’)(leβ€˜π‘Š)𝑣 ↔ 𝑒(leβ€˜π‘‰)(π»β€˜π‘£)))
111110anasss 467 . . 3 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘‰) ∧ 𝑣 ∈ (Baseβ€˜π‘Š))) β†’ ((πΊβ€˜π‘’)(leβ€˜π‘Š)𝑣 ↔ 𝑒(leβ€˜π‘‰)(π»β€˜π‘£)))
112111ralrimivva 3200 . 2 (πœ‘ β†’ βˆ€π‘’ ∈ (Baseβ€˜π‘‰)βˆ€π‘£ ∈ (Baseβ€˜π‘Š)((πΊβ€˜π‘’)(leβ€˜π‘Š)𝑣 ↔ 𝑒(leβ€˜π‘‰)(π»β€˜π‘£)))
113 eqid 2732 . . 3 (Baseβ€˜π‘‰) = (Baseβ€˜π‘‰)
114 eqid 2732 . . 3 (Baseβ€˜π‘Š) = (Baseβ€˜π‘Š)
115 eqid 2732 . . 3 (𝑉MGalConnπ‘Š) = (𝑉MGalConnπ‘Š)
11612ipopos 18491 . . . 4 𝑉 ∈ Poset
117 posprs 18271 . . . 4 (𝑉 ∈ Poset β†’ 𝑉 ∈ Proset )
118116, 117mp1i 13 . . 3 (πœ‘ β†’ 𝑉 ∈ Proset )
11916ipopos 18491 . . . 4 π‘Š ∈ Poset
120 posprs 18271 . . . 4 (π‘Š ∈ Poset β†’ π‘Š ∈ Proset )
121119, 120mp1i 13 . . 3 (πœ‘ β†’ π‘Š ∈ Proset )
122113, 114, 107, 100, 115, 118, 121mgcval 32195 . 2 (πœ‘ β†’ (𝐺(𝑉MGalConnπ‘Š)𝐻 ↔ ((𝐺:(Baseβ€˜π‘‰)⟢(Baseβ€˜π‘Š) ∧ 𝐻:(Baseβ€˜π‘Š)⟢(Baseβ€˜π‘‰)) ∧ βˆ€π‘’ ∈ (Baseβ€˜π‘‰)βˆ€π‘£ ∈ (Baseβ€˜π‘Š)((πΊβ€˜π‘’)(leβ€˜π‘Š)𝑣 ↔ 𝑒(leβ€˜π‘‰)(π»β€˜π‘£)))))
12329, 112, 122mpbir2and 711 1 (πœ‘ β†’ 𝐺(𝑉MGalConnπ‘Š)𝐻)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  βˆ€wral 3061  {crab 3432  Vcvv 3474   βŠ† wss 3948  π’« cpw 4602  {csn 4628   class class class wbr 5148   ↦ cmpt 5231  β—‘ccnv 5675   β€œ cima 5679  Fun wfun 6537   Fn wfn 6538  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7411  Basecbs 17146  lecple 17206   Proset cproset 18248  Posetcpo 18262  toInccipo 18482  MGalConncmgc 32187
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-nn 12215  df-2 12277  df-3 12278  df-4 12279  df-5 12280  df-6 12281  df-7 12282  df-8 12283  df-9 12284  df-n0 12475  df-z 12561  df-dec 12680  df-uz 12825  df-fz 13487  df-struct 17082  df-slot 17117  df-ndx 17129  df-base 17147  df-tset 17218  df-ple 17219  df-ocomp 17220  df-proset 18250  df-poset 18268  df-ipo 18483  df-mgc 32189
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator