MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mrieqv2d Structured version   Visualization version   GIF version
Theorem mrieqv2d 17583
Description: In a Moore system, a set is independent if and only if all its proper subsets have closure properly contained in the closure of the set. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.)
Hypotheses
Ref Expression
mrieqvd.1 (πœ‘ β†’ 𝐴 ∈ (Mooreβ€˜π‘‹))
mrieqvd.2 𝑁 = (mrClsβ€˜π΄)
mrieqvd.3 𝐼 = (mrIndβ€˜π΄)
mrieqvd.4 (πœ‘ β†’ 𝑆 βŠ† 𝑋)
Assertion
Ref Expression
mrieqv2d (πœ‘ β†’ (𝑆 ∈ 𝐼 ↔ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))))
Distinct variable groups:   𝑆,𝑠   πœ‘,𝑠   𝐼,𝑠   𝑁,𝑠
Allowed substitution hints:   𝐴(𝑠)   𝑋(𝑠)
Proof of Theorem mrieqv2d
Dummy variable π‘₯ is distinct from all other variables.
StepHypRef Expression
1 pssnel 4471 . . . . . . 7 (𝑠 ⊊ 𝑆 β†’ βˆƒπ‘₯(π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠))
213ad2ant3 1136 . . . . . 6 ((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) β†’ βˆƒπ‘₯(π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠))
3 mrieqvd.1 . . . . . . . . . 10 (πœ‘ β†’ 𝐴 ∈ (Mooreβ€˜π‘‹))
433ad2ant1 1134 . . . . . . . . 9 ((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) β†’ 𝐴 ∈ (Mooreβ€˜π‘‹))
54adantr 482 . . . . . . . 8 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ 𝐴 ∈ (Mooreβ€˜π‘‹))
6 mrieqvd.2 . . . . . . . 8 𝑁 = (mrClsβ€˜π΄)
7 simprr 772 . . . . . . . . . 10 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ Β¬ π‘₯ ∈ 𝑠)
8 difsnb 4810 . . . . . . . . . 10 (Β¬ π‘₯ ∈ 𝑠 ↔ (𝑠 βˆ– {π‘₯}) = 𝑠)
97, 8sylib 217 . . . . . . . . 9 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ (𝑠 βˆ– {π‘₯}) = 𝑠)
10 simpl3 1194 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ 𝑠 ⊊ 𝑆)
1110pssssd 4098 . . . . . . . . . 10 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ 𝑠 βŠ† 𝑆)
1211ssdifd 4141 . . . . . . . . 9 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ (𝑠 βˆ– {π‘₯}) βŠ† (𝑆 βˆ– {π‘₯}))
139, 12eqsstrrd 4022 . . . . . . . 8 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ 𝑠 βŠ† (𝑆 βˆ– {π‘₯}))
14 mrieqvd.3 . . . . . . . . . 10 𝐼 = (mrIndβ€˜π΄)
15 simpl2 1193 . . . . . . . . . 10 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ 𝑆 ∈ 𝐼)
1614, 5, 15mrissd 17580 . . . . . . . . 9 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ 𝑆 βŠ† 𝑋)
1716ssdifssd 4143 . . . . . . . 8 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ (𝑆 βˆ– {π‘₯}) βŠ† 𝑋)
185, 6, 13, 17mrcssd 17568 . . . . . . 7 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ (π‘β€˜π‘ ) βŠ† (π‘β€˜(𝑆 βˆ– {π‘₯})))
19 difssd 4133 . . . . . . . . 9 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ (𝑆 βˆ– {π‘₯}) βŠ† 𝑆)
205, 6, 19, 16mrcssd 17568 . . . . . . . 8 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ (π‘β€˜(𝑆 βˆ– {π‘₯})) βŠ† (π‘β€˜π‘†))
215, 6, 16mrcssidd 17569 . . . . . . . . 9 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ 𝑆 βŠ† (π‘β€˜π‘†))
22 simprl 770 . . . . . . . . 9 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ π‘₯ ∈ 𝑆)
2321, 22sseldd 3984 . . . . . . . 8 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ π‘₯ ∈ (π‘β€˜π‘†))
246, 14, 5, 15, 22ismri2dad 17581 . . . . . . . 8 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ Β¬ π‘₯ ∈ (π‘β€˜(𝑆 βˆ– {π‘₯})))
2520, 23, 24ssnelpssd 4113 . . . . . . 7 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ (π‘β€˜(𝑆 βˆ– {π‘₯})) ⊊ (π‘β€˜π‘†))
2618, 25sspsstrd 4109 . . . . . 6 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))
272, 26exlimddv 1939 . . . . 5 ((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))
28273expia 1122 . . . 4 ((πœ‘ ∧ 𝑆 ∈ 𝐼) β†’ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)))
2928alrimiv 1931 . . 3 ((πœ‘ ∧ 𝑆 ∈ 𝐼) β†’ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)))
3029ex 414 . 2 (πœ‘ β†’ (𝑆 ∈ 𝐼 β†’ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))))
313adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ 𝐴 ∈ (Mooreβ€˜π‘‹))
3231elfvexd 6931 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ 𝑋 ∈ V)
33 mrieqvd.4 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑆 βŠ† 𝑋)
3433adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ 𝑆 βŠ† 𝑋)
3532, 34ssexd 5325 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ 𝑆 ∈ V)
3635difexd 5330 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ (𝑆 βˆ– {π‘₯}) ∈ V)
37 simp1r 1199 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘₯ ∈ 𝑆) ∧ 𝑠 = (𝑆 βˆ– {π‘₯}) ∧ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ π‘₯ ∈ 𝑆)
38 difsnpss 4811 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ 𝑆 ↔ (𝑆 βˆ– {π‘₯}) ⊊ 𝑆)
3937, 38sylib 217 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ 𝑆) ∧ 𝑠 = (𝑆 βˆ– {π‘₯}) ∧ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ (𝑆 βˆ– {π‘₯}) ⊊ 𝑆)
40 simp2 1138 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘₯ ∈ 𝑆) ∧ 𝑠 = (𝑆 βˆ– {π‘₯}) ∧ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ 𝑠 = (𝑆 βˆ– {π‘₯}))
4140psseq1d 4093 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ 𝑆) ∧ 𝑠 = (𝑆 βˆ– {π‘₯}) ∧ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ (𝑠 ⊊ 𝑆 ↔ (𝑆 βˆ– {π‘₯}) ⊊ 𝑆))
4239, 41mpbird 257 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘₯ ∈ 𝑆) ∧ 𝑠 = (𝑆 βˆ– {π‘₯}) ∧ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ 𝑠 ⊊ 𝑆)
43 simp3 1139 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘₯ ∈ 𝑆) ∧ 𝑠 = (𝑆 βˆ– {π‘₯}) ∧ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)))
4442, 43mpd 15 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ 𝑆) ∧ 𝑠 = (𝑆 βˆ– {π‘₯}) ∧ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))
4540fveq2d 6896 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘₯ ∈ 𝑆) ∧ 𝑠 = (𝑆 βˆ– {π‘₯}) ∧ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ (π‘β€˜π‘ ) = (π‘β€˜(𝑆 βˆ– {π‘₯})))
4645psseq1d 4093 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ 𝑆) ∧ 𝑠 = (𝑆 βˆ– {π‘₯}) ∧ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ ((π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†) ↔ (π‘β€˜(𝑆 βˆ– {π‘₯})) ⊊ (π‘β€˜π‘†)))
4744, 46mpbid 231 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ 𝑆) ∧ 𝑠 = (𝑆 βˆ– {π‘₯}) ∧ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ (π‘β€˜(𝑆 βˆ– {π‘₯})) ⊊ (π‘β€˜π‘†))
48473expia 1122 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ 𝑆) ∧ 𝑠 = (𝑆 βˆ– {π‘₯})) β†’ ((𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)) β†’ (π‘β€˜(𝑆 βˆ– {π‘₯})) ⊊ (π‘β€˜π‘†)))
4936, 48spcimdv 3584 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ (βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)) β†’ (π‘β€˜(𝑆 βˆ– {π‘₯})) ⊊ (π‘β€˜π‘†)))
50493impia 1118 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝑆 ∧ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ (π‘β€˜(𝑆 βˆ– {π‘₯})) ⊊ (π‘β€˜π‘†))
5150pssned 4099 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝑆 ∧ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ (π‘β€˜(𝑆 βˆ– {π‘₯})) β‰  (π‘β€˜π‘†))
52513com23 1127 . . . . . . 7 ((πœ‘ ∧ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)) ∧ π‘₯ ∈ 𝑆) β†’ (π‘β€˜(𝑆 βˆ– {π‘₯})) β‰  (π‘β€˜π‘†))
5333ad2ant1 1134 . . . . . . . . 9 ((πœ‘ ∧ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)) ∧ π‘₯ ∈ 𝑆) β†’ 𝐴 ∈ (Mooreβ€˜π‘‹))
54333ad2ant1 1134 . . . . . . . . 9 ((πœ‘ ∧ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)) ∧ π‘₯ ∈ 𝑆) β†’ 𝑆 βŠ† 𝑋)
55 simp3 1139 . . . . . . . . 9 ((πœ‘ ∧ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)) ∧ π‘₯ ∈ 𝑆) β†’ π‘₯ ∈ 𝑆)
5653, 6, 54, 55mrieqvlemd 17573 . . . . . . . 8 ((πœ‘ ∧ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)) ∧ π‘₯ ∈ 𝑆) β†’ (π‘₯ ∈ (π‘β€˜(𝑆 βˆ– {π‘₯})) ↔ (π‘β€˜(𝑆 βˆ– {π‘₯})) = (π‘β€˜π‘†)))
5756necon3bbid 2979 . . . . . . 7 ((πœ‘ ∧ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)) ∧ π‘₯ ∈ 𝑆) β†’ (Β¬ π‘₯ ∈ (π‘β€˜(𝑆 βˆ– {π‘₯})) ↔ (π‘β€˜(𝑆 βˆ– {π‘₯})) β‰  (π‘β€˜π‘†)))
5852, 57mpbird 257 . . . . . 6 ((πœ‘ ∧ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)) ∧ π‘₯ ∈ 𝑆) β†’ Β¬ π‘₯ ∈ (π‘β€˜(𝑆 βˆ– {π‘₯})))
59583expia 1122 . . . . 5 ((πœ‘ ∧ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ (π‘₯ ∈ 𝑆 β†’ Β¬ π‘₯ ∈ (π‘β€˜(𝑆 βˆ– {π‘₯}))))
6059ralrimiv 3146 . . . 4 ((πœ‘ ∧ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ βˆ€π‘₯ ∈ 𝑆 Β¬ π‘₯ ∈ (π‘β€˜(𝑆 βˆ– {π‘₯})))
6160ex 414 . . 3 (πœ‘ β†’ (βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)) β†’ βˆ€π‘₯ ∈ 𝑆 Β¬ π‘₯ ∈ (π‘β€˜(𝑆 βˆ– {π‘₯}))))
626, 14, 3, 33ismri2d 17577 . . 3 (πœ‘ β†’ (𝑆 ∈ 𝐼 ↔ βˆ€π‘₯ ∈ 𝑆 Β¬ π‘₯ ∈ (π‘β€˜(𝑆 βˆ– {π‘₯}))))
6361, 62sylibrd 259 . 2 (πœ‘ β†’ (βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)) β†’ 𝑆 ∈ 𝐼))
6430, 63impbid 211 1 (πœ‘ β†’ (𝑆 ∈ 𝐼 ↔ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088  βˆ€wal 1540   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  Vcvv 3475   βˆ– cdif 3946   βŠ† wss 3949   ⊊ wpss 3950  {csn 4629  β€˜cfv 6544  Moorecmre 17526  mrClscmrc 17527  mrIndcmri 17528
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 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-mre 17530  df-mrc 17531  df-mri 17532
This theorem is referenced by:  mrissmrcd  17584
  Copyright terms: Public domain W3C validator