MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mrieqv2d Structured version   Visualization version   GIF version
Theorem mrieqv2d 17585
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 4470 . . . . . . 7 (𝑠 ⊊ 𝑆 β†’ βˆƒπ‘₯(π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠))
213ad2ant3 1135 . . . . . 6 ((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) β†’ βˆƒπ‘₯(π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠))
3 mrieqvd.1 . . . . . . . . . 10 (πœ‘ β†’ 𝐴 ∈ (Mooreβ€˜π‘‹))
433ad2ant1 1133 . . . . . . . . 9 ((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) β†’ 𝐴 ∈ (Mooreβ€˜π‘‹))
54adantr 481 . . . . . . . 8 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ 𝐴 ∈ (Mooreβ€˜π‘‹))
6 mrieqvd.2 . . . . . . . 8 𝑁 = (mrClsβ€˜π΄)
7 simprr 771 . . . . . . . . . 10 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ Β¬ π‘₯ ∈ 𝑠)
8 difsnb 4809 . . . . . . . . . 10 (Β¬ π‘₯ ∈ 𝑠 ↔ (𝑠 βˆ– {π‘₯}) = 𝑠)
97, 8sylib 217 . . . . . . . . 9 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ (𝑠 βˆ– {π‘₯}) = 𝑠)
10 simpl3 1193 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ 𝑠 ⊊ 𝑆)
1110pssssd 4097 . . . . . . . . . 10 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ 𝑠 βŠ† 𝑆)
1211ssdifd 4140 . . . . . . . . 9 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ (𝑠 βˆ– {π‘₯}) βŠ† (𝑆 βˆ– {π‘₯}))
139, 12eqsstrrd 4021 . . . . . . . 8 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ 𝑠 βŠ† (𝑆 βˆ– {π‘₯}))
14 mrieqvd.3 . . . . . . . . . 10 𝐼 = (mrIndβ€˜π΄)
15 simpl2 1192 . . . . . . . . . 10 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ 𝑆 ∈ 𝐼)
1614, 5, 15mrissd 17582 . . . . . . . . 9 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ 𝑆 βŠ† 𝑋)
1716ssdifssd 4142 . . . . . . . 8 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ (𝑆 βˆ– {π‘₯}) βŠ† 𝑋)
185, 6, 13, 17mrcssd 17570 . . . . . . 7 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ (π‘β€˜π‘ ) βŠ† (π‘β€˜(𝑆 βˆ– {π‘₯})))
19 difssd 4132 . . . . . . . . 9 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ (𝑆 βˆ– {π‘₯}) βŠ† 𝑆)
205, 6, 19, 16mrcssd 17570 . . . . . . . 8 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ (π‘β€˜(𝑆 βˆ– {π‘₯})) βŠ† (π‘β€˜π‘†))
215, 6, 16mrcssidd 17571 . . . . . . . . 9 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ 𝑆 βŠ† (π‘β€˜π‘†))
22 simprl 769 . . . . . . . . 9 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ π‘₯ ∈ 𝑆)
2321, 22sseldd 3983 . . . . . . . 8 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ π‘₯ ∈ (π‘β€˜π‘†))
246, 14, 5, 15, 22ismri2dad 17583 . . . . . . . 8 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ Β¬ π‘₯ ∈ (π‘β€˜(𝑆 βˆ– {π‘₯})))
2520, 23, 24ssnelpssd 4112 . . . . . . 7 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ (π‘β€˜(𝑆 βˆ– {π‘₯})) ⊊ (π‘β€˜π‘†))
2618, 25sspsstrd 4108 . . . . . 6 (((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) ∧ (π‘₯ ∈ 𝑆 ∧ Β¬ π‘₯ ∈ 𝑠)) β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))
272, 26exlimddv 1938 . . . . 5 ((πœ‘ ∧ 𝑆 ∈ 𝐼 ∧ 𝑠 ⊊ 𝑆) β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))
28273expia 1121 . . . 4 ((πœ‘ ∧ 𝑆 ∈ 𝐼) β†’ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)))
2928alrimiv 1930 . . 3 ((πœ‘ ∧ 𝑆 ∈ 𝐼) β†’ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)))
3029ex 413 . 2 (πœ‘ β†’ (𝑆 ∈ 𝐼 β†’ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))))
313adantr 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ 𝐴 ∈ (Mooreβ€˜π‘‹))
3231elfvexd 6930 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ 𝑋 ∈ V)
33 mrieqvd.4 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑆 βŠ† 𝑋)
3433adantr 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ 𝑆 βŠ† 𝑋)
3532, 34ssexd 5324 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ 𝑆 ∈ V)
3635difexd 5329 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ (𝑆 βˆ– {π‘₯}) ∈ V)
37 simp1r 1198 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘₯ ∈ 𝑆) ∧ 𝑠 = (𝑆 βˆ– {π‘₯}) ∧ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ π‘₯ ∈ 𝑆)
38 difsnpss 4810 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ 𝑆 ↔ (𝑆 βˆ– {π‘₯}) ⊊ 𝑆)
3937, 38sylib 217 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ 𝑆) ∧ 𝑠 = (𝑆 βˆ– {π‘₯}) ∧ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ (𝑆 βˆ– {π‘₯}) ⊊ 𝑆)
40 simp2 1137 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘₯ ∈ 𝑆) ∧ 𝑠 = (𝑆 βˆ– {π‘₯}) ∧ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ 𝑠 = (𝑆 βˆ– {π‘₯}))
4140psseq1d 4092 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ 𝑆) ∧ 𝑠 = (𝑆 βˆ– {π‘₯}) ∧ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ (𝑠 ⊊ 𝑆 ↔ (𝑆 βˆ– {π‘₯}) ⊊ 𝑆))
4239, 41mpbird 256 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘₯ ∈ 𝑆) ∧ 𝑠 = (𝑆 βˆ– {π‘₯}) ∧ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ 𝑠 ⊊ 𝑆)
43 simp3 1138 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘₯ ∈ 𝑆) ∧ 𝑠 = (𝑆 βˆ– {π‘₯}) ∧ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)))
4442, 43mpd 15 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ 𝑆) ∧ 𝑠 = (𝑆 βˆ– {π‘₯}) ∧ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))
4540fveq2d 6895 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘₯ ∈ 𝑆) ∧ 𝑠 = (𝑆 βˆ– {π‘₯}) ∧ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ (π‘β€˜π‘ ) = (π‘β€˜(𝑆 βˆ– {π‘₯})))
4645psseq1d 4092 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ 𝑆) ∧ 𝑠 = (𝑆 βˆ– {π‘₯}) ∧ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ ((π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†) ↔ (π‘β€˜(𝑆 βˆ– {π‘₯})) ⊊ (π‘β€˜π‘†)))
4744, 46mpbid 231 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ 𝑆) ∧ 𝑠 = (𝑆 βˆ– {π‘₯}) ∧ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ (π‘β€˜(𝑆 βˆ– {π‘₯})) ⊊ (π‘β€˜π‘†))
48473expia 1121 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ 𝑆) ∧ 𝑠 = (𝑆 βˆ– {π‘₯})) β†’ ((𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)) β†’ (π‘β€˜(𝑆 βˆ– {π‘₯})) ⊊ (π‘β€˜π‘†)))
4936, 48spcimdv 3583 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ (βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)) β†’ (π‘β€˜(𝑆 βˆ– {π‘₯})) ⊊ (π‘β€˜π‘†)))
50493impia 1117 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝑆 ∧ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ (π‘β€˜(𝑆 βˆ– {π‘₯})) ⊊ (π‘β€˜π‘†))
5150pssned 4098 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝑆 ∧ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ (π‘β€˜(𝑆 βˆ– {π‘₯})) β‰  (π‘β€˜π‘†))
52513com23 1126 . . . . . . 7 ((πœ‘ ∧ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)) ∧ π‘₯ ∈ 𝑆) β†’ (π‘β€˜(𝑆 βˆ– {π‘₯})) β‰  (π‘β€˜π‘†))
5333ad2ant1 1133 . . . . . . . . 9 ((πœ‘ ∧ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)) ∧ π‘₯ ∈ 𝑆) β†’ 𝐴 ∈ (Mooreβ€˜π‘‹))
54333ad2ant1 1133 . . . . . . . . 9 ((πœ‘ ∧ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)) ∧ π‘₯ ∈ 𝑆) β†’ 𝑆 βŠ† 𝑋)
55 simp3 1138 . . . . . . . . 9 ((πœ‘ ∧ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)) ∧ π‘₯ ∈ 𝑆) β†’ π‘₯ ∈ 𝑆)
5653, 6, 54, 55mrieqvlemd 17575 . . . . . . . 8 ((πœ‘ ∧ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)) ∧ π‘₯ ∈ 𝑆) β†’ (π‘₯ ∈ (π‘β€˜(𝑆 βˆ– {π‘₯})) ↔ (π‘β€˜(𝑆 βˆ– {π‘₯})) = (π‘β€˜π‘†)))
5756necon3bbid 2978 . . . . . . 7 ((πœ‘ ∧ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)) ∧ π‘₯ ∈ 𝑆) β†’ (Β¬ π‘₯ ∈ (π‘β€˜(𝑆 βˆ– {π‘₯})) ↔ (π‘β€˜(𝑆 βˆ– {π‘₯})) β‰  (π‘β€˜π‘†)))
5852, 57mpbird 256 . . . . . 6 ((πœ‘ ∧ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)) ∧ π‘₯ ∈ 𝑆) β†’ Β¬ π‘₯ ∈ (π‘β€˜(𝑆 βˆ– {π‘₯})))
59583expia 1121 . . . . 5 ((πœ‘ ∧ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ (π‘₯ ∈ 𝑆 β†’ Β¬ π‘₯ ∈ (π‘β€˜(𝑆 βˆ– {π‘₯}))))
6059ralrimiv 3145 . . . 4 ((πœ‘ ∧ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))) β†’ βˆ€π‘₯ ∈ 𝑆 Β¬ π‘₯ ∈ (π‘β€˜(𝑆 βˆ– {π‘₯})))
6160ex 413 . . 3 (πœ‘ β†’ (βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)) β†’ βˆ€π‘₯ ∈ 𝑆 Β¬ π‘₯ ∈ (π‘β€˜(𝑆 βˆ– {π‘₯}))))
626, 14, 3, 33ismri2d 17579 . . 3 (πœ‘ β†’ (𝑆 ∈ 𝐼 ↔ βˆ€π‘₯ ∈ 𝑆 Β¬ π‘₯ ∈ (π‘β€˜(𝑆 βˆ– {π‘₯}))))
6361, 62sylibrd 258 . 2 (πœ‘ β†’ (βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†)) β†’ 𝑆 ∈ 𝐼))
6430, 63impbid 211 1 (πœ‘ β†’ (𝑆 ∈ 𝐼 ↔ βˆ€π‘ (𝑠 ⊊ 𝑆 β†’ (π‘β€˜π‘ ) ⊊ (π‘β€˜π‘†))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087  βˆ€wal 1539   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  Vcvv 3474   βˆ– cdif 3945   βŠ† wss 3948   ⊊ wpss 3949  {csn 4628  β€˜cfv 6543  Moorecmre 17528  mrClscmrc 17529  mrIndcmri 17530
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-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  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-ral 3062  df-rex 3071  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-int 4951  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  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-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-mre 17532  df-mrc 17533  df-mri 17534
This theorem is referenced by:  mrissmrcd  17586
  Copyright terms: Public domain W3C validator