Description: A pair formed of two nested sets is a Moore collection. (Note that in the statement, if B is a proper class, we are in the case of bj-snmoore ). A direct consequence is |- { (/) , A } e. Moore_ .
More generally, any nonempty well-ordered chain of sets that is a set is a Moore collection.
We also have the biconditional |- ( ( A i^i B ) e. V -> ( { A , B } e. Moore_ <-> ( A C_ B \/ B C_ A ) ) ) . (Contributed by BJ, 11-Apr-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-prmoore | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) → { 𝐴 , 𝐵 } ∈ Moore ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm3.22 | ⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V ) ) | |
| 2 | 1 | adantrr | ⊢ ( ( 𝐵 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V ) ) |
| 3 | uniprg | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) ) | |
| 4 | 2 3 | syl | ⊢ ( ( 𝐵 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) ) |
| 5 | simprr | ⊢ ( ( 𝐵 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) ) → 𝐴 ⊆ 𝐵 ) | |
| 6 | ssequn1 | ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∪ 𝐵 ) = 𝐵 ) | |
| 7 | 5 6 | sylib | ⊢ ( ( 𝐵 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) ) → ( 𝐴 ∪ 𝐵 ) = 𝐵 ) |
| 8 | 4 7 | eqtrd | ⊢ ( ( 𝐵 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) ) → ∪ { 𝐴 , 𝐵 } = 𝐵 ) |
| 9 | prid2g | ⊢ ( 𝐵 ∈ V → 𝐵 ∈ { 𝐴 , 𝐵 } ) | |
| 10 | 9 | adantr | ⊢ ( ( 𝐵 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) ) → 𝐵 ∈ { 𝐴 , 𝐵 } ) |
| 11 | 8 10 | eqeltrd | ⊢ ( ( 𝐵 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) ) → ∪ { 𝐴 , 𝐵 } ∈ { 𝐴 , 𝐵 } ) |
| 12 | biid | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) ↔ ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) ) | |
| 13 | 12 | bianass | ⊢ ( ( 𝐵 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) ) ↔ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐴 ⊆ 𝐵 ) ) |
| 14 | inteq | ⊢ ( 𝑥 = { 𝐴 } → ∩ 𝑥 = ∩ { 𝐴 } ) | |
| 15 | intsng | ⊢ ( 𝐴 ∈ 𝑉 → ∩ { 𝐴 } = 𝐴 ) | |
| 16 | 15 | adantl | ⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ∩ { 𝐴 } = 𝐴 ) |
| 17 | 14 16 | sylan9eqr | ⊢ ( ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 = { 𝐴 } ) → ∩ 𝑥 = 𝐴 ) |
| 18 | prid1g | ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 , 𝐵 } ) | |
| 19 | 18 | adantl | ⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ { 𝐴 , 𝐵 } ) |
| 20 | 19 | adantr | ⊢ ( ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 = { 𝐴 } ) → 𝐴 ∈ { 𝐴 , 𝐵 } ) |
| 21 | 17 20 | eqeltrd | ⊢ ( ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 = { 𝐴 } ) → ∩ 𝑥 ∈ { 𝐴 , 𝐵 } ) |
| 22 | 21 | ex | ⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 = { 𝐴 } → ∩ 𝑥 ∈ { 𝐴 , 𝐵 } ) ) |
| 23 | 22 | adantr | ⊢ ( ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑥 = { 𝐴 } → ∩ 𝑥 ∈ { 𝐴 , 𝐵 } ) ) |
| 24 | inteq | ⊢ ( 𝑥 = { 𝐵 } → ∩ 𝑥 = ∩ { 𝐵 } ) | |
| 25 | intsng | ⊢ ( 𝐵 ∈ V → ∩ { 𝐵 } = 𝐵 ) | |
| 26 | 25 | adantr | ⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ∩ { 𝐵 } = 𝐵 ) |
| 27 | 24 26 | sylan9eqr | ⊢ ( ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 = { 𝐵 } ) → ∩ 𝑥 = 𝐵 ) |
| 28 | 9 | ad2antrr | ⊢ ( ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 = { 𝐵 } ) → 𝐵 ∈ { 𝐴 , 𝐵 } ) |
| 29 | 27 28 | eqeltrd | ⊢ ( ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 = { 𝐵 } ) → ∩ 𝑥 ∈ { 𝐴 , 𝐵 } ) |
| 30 | 29 | ex | ⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 = { 𝐵 } → ∩ 𝑥 ∈ { 𝐴 , 𝐵 } ) ) |
| 31 | 30 | adantr | ⊢ ( ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑥 = { 𝐵 } → ∩ 𝑥 ∈ { 𝐴 , 𝐵 } ) ) |
| 32 | inteq | ⊢ ( 𝑥 = { 𝐴 , 𝐵 } → ∩ 𝑥 = ∩ { 𝐴 , 𝐵 } ) | |
| 33 | 32 | adantl | ⊢ ( ( ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 = { 𝐴 , 𝐵 } ) → ∩ 𝑥 = ∩ { 𝐴 , 𝐵 } ) |
| 34 | 1 | ad2antrr | ⊢ ( ( ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 = { 𝐴 , 𝐵 } ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V ) ) |
| 35 | intprg | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V ) → ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 ) ) | |
| 36 | 34 35 | syl | ⊢ ( ( ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 = { 𝐴 , 𝐵 } ) → ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 ) ) |
| 37 | dfss2 | ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐴 ) | |
| 38 | 37 | biimpi | ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∩ 𝐵 ) = 𝐴 ) |
| 39 | 38 | adantl | ⊢ ( ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) = 𝐴 ) |
| 40 | 39 | adantr | ⊢ ( ( ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 = { 𝐴 , 𝐵 } ) → ( 𝐴 ∩ 𝐵 ) = 𝐴 ) |
| 41 | 33 36 40 | 3eqtrd | ⊢ ( ( ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 = { 𝐴 , 𝐵 } ) → ∩ 𝑥 = 𝐴 ) |
| 42 | 18 | ad3antlr | ⊢ ( ( ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 = { 𝐴 , 𝐵 } ) → 𝐴 ∈ { 𝐴 , 𝐵 } ) |
| 43 | 41 42 | eqeltrd | ⊢ ( ( ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 = { 𝐴 , 𝐵 } ) → ∩ 𝑥 ∈ { 𝐴 , 𝐵 } ) |
| 44 | 43 | ex | ⊢ ( ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑥 = { 𝐴 , 𝐵 } → ∩ 𝑥 ∈ { 𝐴 , 𝐵 } ) ) |
| 45 | 31 44 | jaod | ⊢ ( ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝑥 = { 𝐵 } ∨ 𝑥 = { 𝐴 , 𝐵 } ) → ∩ 𝑥 ∈ { 𝐴 , 𝐵 } ) ) |
| 46 | 23 45 | jaod | ⊢ ( ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝑥 = { 𝐴 } ∨ ( 𝑥 = { 𝐵 } ∨ 𝑥 = { 𝐴 , 𝐵 } ) ) → ∩ 𝑥 ∈ { 𝐴 , 𝐵 } ) ) |
| 47 | sspr | ⊢ ( 𝑥 ⊆ { 𝐴 , 𝐵 } ↔ ( ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) ∨ ( 𝑥 = { 𝐵 } ∨ 𝑥 = { 𝐴 , 𝐵 } ) ) ) | |
| 48 | andir | ⊢ ( ( ( ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) ∨ ( 𝑥 = { 𝐵 } ∨ 𝑥 = { 𝐴 , 𝐵 } ) ) ∧ 𝑥 ≠ ∅ ) ↔ ( ( ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) ∧ 𝑥 ≠ ∅ ) ∨ ( ( 𝑥 = { 𝐵 } ∨ 𝑥 = { 𝐴 , 𝐵 } ) ∧ 𝑥 ≠ ∅ ) ) ) | |
| 49 | andir | ⊢ ( ( ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) ∧ 𝑥 ≠ ∅ ) ↔ ( ( 𝑥 = ∅ ∧ 𝑥 ≠ ∅ ) ∨ ( 𝑥 = { 𝐴 } ∧ 𝑥 ≠ ∅ ) ) ) | |
| 50 | eqneqall | ⊢ ( 𝑥 = ∅ → ( 𝑥 ≠ ∅ → ⊥ ) ) | |
| 51 | 50 | imp | ⊢ ( ( 𝑥 = ∅ ∧ 𝑥 ≠ ∅ ) → ⊥ ) |
| 52 | simpl | ⊢ ( ( 𝑥 = { 𝐴 } ∧ 𝑥 ≠ ∅ ) → 𝑥 = { 𝐴 } ) | |
| 53 | 51 52 | orim12i | ⊢ ( ( ( 𝑥 = ∅ ∧ 𝑥 ≠ ∅ ) ∨ ( 𝑥 = { 𝐴 } ∧ 𝑥 ≠ ∅ ) ) → ( ⊥ ∨ 𝑥 = { 𝐴 } ) ) |
| 54 | falim | ⊢ ( ⊥ → 𝑥 = { 𝐴 } ) | |
| 55 | 54 | bj-jaoi1 | ⊢ ( ( ⊥ ∨ 𝑥 = { 𝐴 } ) → 𝑥 = { 𝐴 } ) |
| 56 | 53 55 | syl | ⊢ ( ( ( 𝑥 = ∅ ∧ 𝑥 ≠ ∅ ) ∨ ( 𝑥 = { 𝐴 } ∧ 𝑥 ≠ ∅ ) ) → 𝑥 = { 𝐴 } ) |
| 57 | 49 56 | sylbi | ⊢ ( ( ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) ∧ 𝑥 ≠ ∅ ) → 𝑥 = { 𝐴 } ) |
| 58 | simpl | ⊢ ( ( ( 𝑥 = { 𝐵 } ∨ 𝑥 = { 𝐴 , 𝐵 } ) ∧ 𝑥 ≠ ∅ ) → ( 𝑥 = { 𝐵 } ∨ 𝑥 = { 𝐴 , 𝐵 } ) ) | |
| 59 | 57 58 | orim12i | ⊢ ( ( ( ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) ∧ 𝑥 ≠ ∅ ) ∨ ( ( 𝑥 = { 𝐵 } ∨ 𝑥 = { 𝐴 , 𝐵 } ) ∧ 𝑥 ≠ ∅ ) ) → ( 𝑥 = { 𝐴 } ∨ ( 𝑥 = { 𝐵 } ∨ 𝑥 = { 𝐴 , 𝐵 } ) ) ) |
| 60 | 48 59 | sylbi | ⊢ ( ( ( ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) ∨ ( 𝑥 = { 𝐵 } ∨ 𝑥 = { 𝐴 , 𝐵 } ) ) ∧ 𝑥 ≠ ∅ ) → ( 𝑥 = { 𝐴 } ∨ ( 𝑥 = { 𝐵 } ∨ 𝑥 = { 𝐴 , 𝐵 } ) ) ) |
| 61 | 47 60 | sylanb | ⊢ ( ( 𝑥 ⊆ { 𝐴 , 𝐵 } ∧ 𝑥 ≠ ∅ ) → ( 𝑥 = { 𝐴 } ∨ ( 𝑥 = { 𝐵 } ∨ 𝑥 = { 𝐴 , 𝐵 } ) ) ) |
| 62 | 46 61 | impel | ⊢ ( ( ( ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ( 𝑥 ⊆ { 𝐴 , 𝐵 } ∧ 𝑥 ≠ ∅ ) ) → ∩ 𝑥 ∈ { 𝐴 , 𝐵 } ) |
| 63 | 13 62 | sylanb | ⊢ ( ( ( 𝐵 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) ) ∧ ( 𝑥 ⊆ { 𝐴 , 𝐵 } ∧ 𝑥 ≠ ∅ ) ) → ∩ 𝑥 ∈ { 𝐴 , 𝐵 } ) |
| 64 | 11 63 | bj-ismooredr2 | ⊢ ( ( 𝐵 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) ) → { 𝐴 , 𝐵 } ∈ Moore ) |
| 65 | pm3.22 | ⊢ ( ( ¬ 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V ) ) | |
| 66 | 65 | adantrr | ⊢ ( ( ¬ 𝐵 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) ) → ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V ) ) |
| 67 | prprc2 | ⊢ ( ¬ 𝐵 ∈ V → { 𝐴 , 𝐵 } = { 𝐴 } ) | |
| 68 | 67 | adantl | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V ) → { 𝐴 , 𝐵 } = { 𝐴 } ) |
| 69 | 68 | eqcomd | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V ) → { 𝐴 } = { 𝐴 , 𝐵 } ) |
| 70 | 66 69 | syl | ⊢ ( ( ¬ 𝐵 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) ) → { 𝐴 } = { 𝐴 , 𝐵 } ) |
| 71 | bj-snmoore | ⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ∈ Moore ) | |
| 72 | 71 | ad2antrl | ⊢ ( ( ¬ 𝐵 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) ) → { 𝐴 } ∈ Moore ) |
| 73 | 70 72 | eqeltrrd | ⊢ ( ( ¬ 𝐵 ∈ V ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) ) → { 𝐴 , 𝐵 } ∈ Moore ) |
| 74 | 64 73 | pm2.61ian | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) → { 𝐴 , 𝐵 } ∈ Moore ) |