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 31563
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 6023 . . . . . . . 8 (𝐹𝑛) ⊆ dom 𝐹
4 pwrssmgc.7 . . . . . . . 8 (𝜑𝐹:𝑋𝑌)
53, 4fssdm 6675 . . . . . . 7 (𝜑 → (𝐹𝑛) ⊆ 𝑋)
65adantr 482 . . . . . 6 ((𝜑𝑛 ∈ 𝒫 𝑌) → (𝐹𝑛) ⊆ 𝑋)
72, 6sselpwd 5274 . . . . 5 ((𝜑𝑛 ∈ 𝒫 𝑌) → (𝐹𝑛) ∈ 𝒫 𝑋)
8 pwrssmgc.1 . . . . 5 𝐺 = (𝑛 ∈ 𝒫 𝑌 ↦ (𝐹𝑛))
97, 8fmptd 7048 . . . 4 (𝜑𝐺:𝒫 𝑌⟶𝒫 𝑋)
10 pwrssmgc.6 . . . . . 6 (𝜑𝑌𝐵)
11 pwexg 5325 . . . . . 6 (𝑌𝐵 → 𝒫 𝑌 ∈ V)
12 pwrssmgc.3 . . . . . . 7 𝑉 = (toInc‘𝒫 𝑌)
1312ipobas 18346 . . . . . 6 (𝒫 𝑌 ∈ V → 𝒫 𝑌 = (Base‘𝑉))
1410, 11, 133syl 18 . . . . 5 (𝜑 → 𝒫 𝑌 = (Base‘𝑉))
15 pwexg 5325 . . . . . 6 (𝑋𝐴 → 𝒫 𝑋 ∈ V)
16 pwrssmgc.4 . . . . . . 7 𝑊 = (toInc‘𝒫 𝑋)
1716ipobas 18346 . . . . . 6 (𝒫 𝑋 ∈ V → 𝒫 𝑋 = (Base‘𝑊))
181, 15, 173syl 18 . . . . 5 (𝜑 → 𝒫 𝑋 = (Base‘𝑊))
1914, 18feq23d 6650 . . . 4 (𝜑 → (𝐺:𝒫 𝑌⟶𝒫 𝑋𝐺:(Base‘𝑉)⟶(Base‘𝑊)))
209, 19mpbid 231 . . 3 (𝜑𝐺:(Base‘𝑉)⟶(Base‘𝑊))
2110adantr 482 . . . . . 6 ((𝜑𝑚 ∈ 𝒫 𝑋) → 𝑌𝐵)
22 ssrab2 4028 . . . . . . 7 {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑚} ⊆ 𝑌
2322a1i 11 . . . . . 6 ((𝜑𝑚 ∈ 𝒫 𝑋) → {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑚} ⊆ 𝑌)
2421, 23sselpwd 5274 . . . . 5 ((𝜑𝑚 ∈ 𝒫 𝑋) → {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑚} ∈ 𝒫 𝑌)
25 pwrssmgc.2 . . . . 5 𝐻 = (𝑚 ∈ 𝒫 𝑋 ↦ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑚})
2624, 25fmptd 7048 . . . 4 (𝜑𝐻:𝒫 𝑋⟶𝒫 𝑌)
2718, 14feq23d 6650 . . . 4 (𝜑 → (𝐻:𝒫 𝑋⟶𝒫 𝑌𝐻:(Base‘𝑊)⟶(Base‘𝑉)))
2826, 27mpbid 231 . . 3 (𝜑𝐻:(Base‘𝑊)⟶(Base‘𝑉))
2920, 28jca 513 . 2 (𝜑 → (𝐺:(Base‘𝑉)⟶(Base‘𝑊) ∧ 𝐻:(Base‘𝑊)⟶(Base‘𝑉)))
30 sneq 4587 . . . . . . . . . . . 12 (𝑦 = 𝑗 → {𝑦} = {𝑗})
3130imaeq2d 6003 . . . . . . . . . . 11 (𝑦 = 𝑗 → (𝐹 “ {𝑦}) = (𝐹 “ {𝑗}))
3231sseq1d 3966 . . . . . . . . . 10 (𝑦 = 𝑗 → ((𝐹 “ {𝑦}) ⊆ 𝑣 ↔ (𝐹 “ {𝑗}) ⊆ 𝑣))
33 simplr 767 . . . . . . . . . . . . . 14 (((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) → 𝑢 ∈ (Base‘𝑉))
3414ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) → 𝒫 𝑌 = (Base‘𝑉))
3533, 34eleqtrrd 2841 . . . . . . . . . . . . 13 (((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) → 𝑢 ∈ 𝒫 𝑌)
3635adantr 482 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ (𝐹𝑢) ⊆ 𝑣) → 𝑢 ∈ 𝒫 𝑌)
3736elpwid 4560 . . . . . . . . . . 11 ((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ (𝐹𝑢) ⊆ 𝑣) → 𝑢𝑌)
3837sselda 3935 . . . . . . . . . 10 (((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ (𝐹𝑢) ⊆ 𝑣) ∧ 𝑗𝑢) → 𝑗𝑌)
394ffund 6659 . . . . . . . . . . . . 13 (𝜑 → Fun 𝐹)
4039ad4antr 730 . . . . . . . . . . . 12 (((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ (𝐹𝑢) ⊆ 𝑣) ∧ 𝑗𝑢) → Fun 𝐹)
41 snssi 4759 . . . . . . . . . . . . 13 (𝑗𝑢 → {𝑗} ⊆ 𝑢)
4241adantl 483 . . . . . . . . . . . 12 (((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ (𝐹𝑢) ⊆ 𝑣) ∧ 𝑗𝑢) → {𝑗} ⊆ 𝑢)
43 sspreima 7005 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ {𝑗} ⊆ 𝑢) → (𝐹 “ {𝑗}) ⊆ (𝐹𝑢))
4440, 42, 43syl2anc 585 . . . . . . . . . . 11 (((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ (𝐹𝑢) ⊆ 𝑣) ∧ 𝑗𝑢) → (𝐹 “ {𝑗}) ⊆ (𝐹𝑢))
45 simplr 767 . . . . . . . . . . 11 (((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ (𝐹𝑢) ⊆ 𝑣) ∧ 𝑗𝑢) → (𝐹𝑢) ⊆ 𝑣)
4644, 45sstrd 3945 . . . . . . . . . 10 (((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ (𝐹𝑢) ⊆ 𝑣) ∧ 𝑗𝑢) → (𝐹 “ {𝑗}) ⊆ 𝑣)
4732, 38, 46elrabd 3639 . . . . . . . . 9 (((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ (𝐹𝑢) ⊆ 𝑣) ∧ 𝑗𝑢) → 𝑗 ∈ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣})
4847ex 414 . . . . . . . 8 ((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ (𝐹𝑢) ⊆ 𝑣) → (𝑗𝑢𝑗 ∈ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣}))
4948ssrdv 3941 . . . . . . 7 ((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ (𝐹𝑢) ⊆ 𝑣) → 𝑢 ⊆ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣})
50 simplr 767 . . . . . . . . . . . 12 (((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑢 ⊆ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣}) ∧ 𝑖 ∈ (𝐹𝑢)) → 𝑢 ⊆ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣})
514ffnd 6656 . . . . . . . . . . . . . . 15 (𝜑𝐹 Fn 𝑋)
5251ad4antr 730 . . . . . . . . . . . . . 14 (((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑢 ⊆ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣}) ∧ 𝑖 ∈ (𝐹𝑢)) → 𝐹 Fn 𝑋)
53 simpr 486 . . . . . . . . . . . . . 14 (((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑢 ⊆ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣}) ∧ 𝑖 ∈ (𝐹𝑢)) → 𝑖 ∈ (𝐹𝑢))
54 elpreima 6995 . . . . . . . . . . . . . . 15 (𝐹 Fn 𝑋 → (𝑖 ∈ (𝐹𝑢) ↔ (𝑖𝑋 ∧ (𝐹𝑖) ∈ 𝑢)))
5554biimpa 478 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝑋𝑖 ∈ (𝐹𝑢)) → (𝑖𝑋 ∧ (𝐹𝑖) ∈ 𝑢))
5652, 53, 55syl2anc 585 . . . . . . . . . . . . 13 (((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑢 ⊆ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣}) ∧ 𝑖 ∈ (𝐹𝑢)) → (𝑖𝑋 ∧ (𝐹𝑖) ∈ 𝑢))
5756simprd 497 . . . . . . . . . . . 12 (((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑢 ⊆ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣}) ∧ 𝑖 ∈ (𝐹𝑢)) → (𝐹𝑖) ∈ 𝑢)
5850, 57sseldd 3936 . . . . . . . . . . 11 (((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑢 ⊆ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣}) ∧ 𝑖 ∈ (𝐹𝑢)) → (𝐹𝑖) ∈ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣})
59 sneq 4587 . . . . . . . . . . . . . . 15 (𝑦 = (𝐹𝑖) → {𝑦} = {(𝐹𝑖)})
6059imaeq2d 6003 . . . . . . . . . . . . . 14 (𝑦 = (𝐹𝑖) → (𝐹 “ {𝑦}) = (𝐹 “ {(𝐹𝑖)}))
6160sseq1d 3966 . . . . . . . . . . . . 13 (𝑦 = (𝐹𝑖) → ((𝐹 “ {𝑦}) ⊆ 𝑣 ↔ (𝐹 “ {(𝐹𝑖)}) ⊆ 𝑣))
6261elrab 3637 . . . . . . . . . . . 12 ((𝐹𝑖) ∈ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣} ↔ ((𝐹𝑖) ∈ 𝑌 ∧ (𝐹 “ {(𝐹𝑖)}) ⊆ 𝑣))
6362simprbi 498 . . . . . . . . . . 11 ((𝐹𝑖) ∈ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣} → (𝐹 “ {(𝐹𝑖)}) ⊆ 𝑣)
6458, 63syl 17 . . . . . . . . . 10 (((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑢 ⊆ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣}) ∧ 𝑖 ∈ (𝐹𝑢)) → (𝐹 “ {(𝐹𝑖)}) ⊆ 𝑣)
6556simpld 496 . . . . . . . . . . 11 (((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑢 ⊆ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣}) ∧ 𝑖 ∈ (𝐹𝑢)) → 𝑖𝑋)
66 eqidd 2738 . . . . . . . . . . 11 (((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑢 ⊆ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣}) ∧ 𝑖 ∈ (𝐹𝑢)) → (𝐹𝑖) = (𝐹𝑖))
67 fniniseg 6997 . . . . . . . . . . . 12 (𝐹 Fn 𝑋 → (𝑖 ∈ (𝐹 “ {(𝐹𝑖)}) ↔ (𝑖𝑋 ∧ (𝐹𝑖) = (𝐹𝑖))))
6867biimpar 479 . . . . . . . . . . 11 ((𝐹 Fn 𝑋 ∧ (𝑖𝑋 ∧ (𝐹𝑖) = (𝐹𝑖))) → 𝑖 ∈ (𝐹 “ {(𝐹𝑖)}))
6952, 65, 66, 68syl12anc 835 . . . . . . . . . 10 (((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑢 ⊆ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣}) ∧ 𝑖 ∈ (𝐹𝑢)) → 𝑖 ∈ (𝐹 “ {(𝐹𝑖)}))
7064, 69sseldd 3936 . . . . . . . . 9 (((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑢 ⊆ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣}) ∧ 𝑖 ∈ (𝐹𝑢)) → 𝑖𝑣)
7170ex 414 . . . . . . . 8 ((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑢 ⊆ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣}) → (𝑖 ∈ (𝐹𝑢) → 𝑖𝑣))
7271ssrdv 3941 . . . . . . 7 ((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑢 ⊆ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣}) → (𝐹𝑢) ⊆ 𝑣)
7349, 72impbida 799 . . . . . 6 (((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) → ((𝐹𝑢) ⊆ 𝑣𝑢 ⊆ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣}))
74 simpr 486 . . . . . . . . 9 ((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑛 = 𝑢) → 𝑛 = 𝑢)
7574imaeq2d 6003 . . . . . . . 8 ((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑛 = 𝑢) → (𝐹𝑛) = (𝐹𝑢))
764, 1fexd 7163 . . . . . . . . . 10 (𝜑𝐹 ∈ V)
77 cnvexg 7843 . . . . . . . . . 10 (𝐹 ∈ V → 𝐹 ∈ V)
78 imaexg 7834 . . . . . . . . . 10 (𝐹 ∈ V → (𝐹𝑢) ∈ V)
7976, 77, 783syl 18 . . . . . . . . 9 (𝜑 → (𝐹𝑢) ∈ V)
8079ad2antrr 724 . . . . . . . 8 (((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) → (𝐹𝑢) ∈ V)
818, 75, 35, 80fvmptd2 6943 . . . . . . 7 (((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) → (𝐺𝑢) = (𝐹𝑢))
8281sseq1d 3966 . . . . . 6 (((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) → ((𝐺𝑢) ⊆ 𝑣 ↔ (𝐹𝑢) ⊆ 𝑣))
83 simpr 486 . . . . . . . . . 10 ((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑚 = 𝑣) → 𝑚 = 𝑣)
8483sseq2d 3967 . . . . . . . . 9 ((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑚 = 𝑣) → ((𝐹 “ {𝑦}) ⊆ 𝑚 ↔ (𝐹 “ {𝑦}) ⊆ 𝑣))
8584rabbidv 3412 . . . . . . . 8 ((((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑚 = 𝑣) → {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑚} = {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣})
86 simpr 486 . . . . . . . . 9 (((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) → 𝑣 ∈ (Base‘𝑊))
871, 15syl 17 . . . . . . . . . . 11 (𝜑 → 𝒫 𝑋 ∈ V)
8887ad2antrr 724 . . . . . . . . . 10 (((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) → 𝒫 𝑋 ∈ V)
8988, 17syl 17 . . . . . . . . 9 (((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) → 𝒫 𝑋 = (Base‘𝑊))
9086, 89eleqtrrd 2841 . . . . . . . 8 (((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) → 𝑣 ∈ 𝒫 𝑋)
9110ad2antrr 724 . . . . . . . . 9 (((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) → 𝑌𝐵)
92 ssrab2 4028 . . . . . . . . . 10 {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣} ⊆ 𝑌
9392a1i 11 . . . . . . . . 9 (((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) → {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣} ⊆ 𝑌)
9491, 93sselpwd 5274 . . . . . . . 8 (((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) → {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣} ∈ 𝒫 𝑌)
9525, 85, 90, 94fvmptd2 6943 . . . . . . 7 (((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) → (𝐻𝑣) = {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣})
9695sseq2d 3967 . . . . . 6 (((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) → (𝑢 ⊆ (𝐻𝑣) ↔ 𝑢 ⊆ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑣}))
9773, 82, 963bitr4d 311 . . . . 5 (((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) → ((𝐺𝑢) ⊆ 𝑣𝑢 ⊆ (𝐻𝑣)))
989ad2antrr 724 . . . . . . 7 (((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) → 𝐺:𝒫 𝑌⟶𝒫 𝑋)
9998, 35ffvelcdmd 7022 . . . . . 6 (((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) → (𝐺𝑢) ∈ 𝒫 𝑋)
100 eqid 2737 . . . . . . 7 (le‘𝑊) = (le‘𝑊)
10116, 100ipole 18349 . . . . . 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 7022 . . . . . 6 (((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) → (𝐻𝑣) ∈ 𝒫 𝑌)
107 eqid 2737 . . . . . . 7 (le‘𝑉) = (le‘𝑉)
10812, 107ipole 18349 . . . . . 6 ((𝒫 𝑌 ∈ V ∧ 𝑢 ∈ 𝒫 𝑌 ∧ (𝐻𝑣) ∈ 𝒫 𝑌) → (𝑢(le‘𝑉)(𝐻𝑣) ↔ 𝑢 ⊆ (𝐻𝑣)))
109104, 35, 106, 108syl3anc 1371 . . . . 5 (((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) → (𝑢(le‘𝑉)(𝐻𝑣) ↔ 𝑢 ⊆ (𝐻𝑣)))
11097, 102, 1093bitr4d 311 . . . 4 (((𝜑𝑢 ∈ (Base‘𝑉)) ∧ 𝑣 ∈ (Base‘𝑊)) → ((𝐺𝑢)(le‘𝑊)𝑣𝑢(le‘𝑉)(𝐻𝑣)))
111110anasss 468 . . 3 ((𝜑 ∧ (𝑢 ∈ (Base‘𝑉) ∧ 𝑣 ∈ (Base‘𝑊))) → ((𝐺𝑢)(le‘𝑊)𝑣𝑢(le‘𝑉)(𝐻𝑣)))
112111ralrimivva 3194 . 2 (𝜑 → ∀𝑢 ∈ (Base‘𝑉)∀𝑣 ∈ (Base‘𝑊)((𝐺𝑢)(le‘𝑊)𝑣𝑢(le‘𝑉)(𝐻𝑣)))
113 eqid 2737 . . 3 (Base‘𝑉) = (Base‘𝑉)
114 eqid 2737 . . 3 (Base‘𝑊) = (Base‘𝑊)
115 eqid 2737 . . 3 (𝑉MGalConn𝑊) = (𝑉MGalConn𝑊)
11612ipopos 18351 . . . 4 𝑉 ∈ Poset
117 posprs 18131 . . . 4 (𝑉 ∈ Poset → 𝑉 ∈ Proset )
118116, 117mp1i 13 . . 3 (𝜑𝑉 ∈ Proset )
11916ipopos 18351 . . . 4 𝑊 ∈ Poset
120 posprs 18131 . . . 4 (𝑊 ∈ Poset → 𝑊 ∈ Proset )
121119, 120mp1i 13 . . 3 (𝜑𝑊 ∈ Proset )
122113, 114, 107, 100, 115, 118, 121mgcval 31550 . 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 397   = wceq 1541  wcel 2106  wral 3062  {crab 3404  Vcvv 3442  wss 3901  𝒫 cpw 4551  {csn 4577   class class class wbr 5096  cmpt 5179  ccnv 5623  cima 5627  Fun wfun 6477   Fn wfn 6478  wf 6479  cfv 6483  (class class class)co 7341  Basecbs 17009  lecple 17066   Proset cproset 18108  Posetcpo 18122  toInccipo 18342  MGalConncmgc 31542
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 2708  ax-rep 5233  ax-sep 5247  ax-nul 5254  ax-pow 5312  ax-pr 5376  ax-un 7654  ax-cnex 11032  ax-resscn 11033  ax-1cn 11034  ax-icn 11035  ax-addcl 11036  ax-addrcl 11037  ax-mulcl 11038  ax-mulrcl 11039  ax-mulcom 11040  ax-addass 11041  ax-mulass 11042  ax-distr 11043  ax-i2m1 11044  ax-1ne0 11045  ax-1rid 11046  ax-rnegex 11047  ax-rrecex 11048  ax-cnre 11049  ax-pre-lttri 11050  ax-pre-lttrn 11051  ax-pre-ltadd 11052  ax-pre-mulgt0 11053
This theorem depends on definitions:  df-bi 206  df-an 398  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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3351  df-rab 3405  df-v 3444  df-sbc 3731  df-csb 3847  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3920  df-nul 4274  df-if 4478  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4857  df-iun 4947  df-br 5097  df-opab 5159  df-mpt 5180  df-tr 5214  df-id 5522  df-eprel 5528  df-po 5536  df-so 5537  df-fr 5579  df-we 5581  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6242  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6435  df-fun 6485  df-fn 6486  df-f 6487  df-f1 6488  df-fo 6489  df-f1o 6490  df-fv 6491  df-riota 7297  df-ov 7344  df-oprab 7345  df-mpo 7346  df-om 7785  df-1st 7903  df-2nd 7904  df-frecs 8171  df-wrecs 8202  df-recs 8276  df-rdg 8315  df-1o 8371  df-er 8573  df-map 8692  df-en 8809  df-dom 8810  df-sdom 8811  df-fin 8812  df-pnf 11116  df-mnf 11117  df-xr 11118  df-ltxr 11119  df-le 11120  df-sub 11312  df-neg 11313  df-nn 12079  df-2 12141  df-3 12142  df-4 12143  df-5 12144  df-6 12145  df-7 12146  df-8 12147  df-9 12148  df-n0 12339  df-z 12425  df-dec 12543  df-uz 12688  df-fz 13345  df-struct 16945  df-slot 16980  df-ndx 16992  df-base 17010  df-tset 17078  df-ple 17079  df-ocomp 17080  df-proset 18110  df-poset 18128  df-ipo 18343  df-mgc 31544
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator