Metamath Proof Explorer

Theorem bj-prmoore

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 
|- ( ( A e. V /\ A C_ B ) -> { A , B } e. Moore_ )

Proof

Step Hyp Ref Expression
1 pm3.22 
 |-  ( ( B e. _V /\ A e. V ) -> ( A e. V /\ B e. _V ) )
2 1 adantrr 
 |-  ( ( B e. _V /\ ( A e. V /\ A C_ B ) ) -> ( A e. V /\ B e. _V ) )
3 uniprg 
 |-  ( ( A e. V /\ B e. _V ) -> U. { A , B } = ( A u. B ) )
4 2 3 syl 
 |-  ( ( B e. _V /\ ( A e. V /\ A C_ B ) ) -> U. { A , B } = ( A u. B ) )
5 simprr 
 |-  ( ( B e. _V /\ ( A e. V /\ A C_ B ) ) -> A C_ B )
6 ssequn1 
 |-  ( A C_ B <-> ( A u. B ) = B )
7 5 6 sylib 
 |-  ( ( B e. _V /\ ( A e. V /\ A C_ B ) ) -> ( A u. B ) = B )
8 4 7 eqtrd 
 |-  ( ( B e. _V /\ ( A e. V /\ A C_ B ) ) -> U. { A , B } = B )
9 prid2g 
 |-  ( B e. _V -> B e. { A , B } )
10 9 adantr 
 |-  ( ( B e. _V /\ ( A e. V /\ A C_ B ) ) -> B e. { A , B } )
11 8 10 eqeltrd 
 |-  ( ( B e. _V /\ ( A e. V /\ A C_ B ) ) -> U. { A , B } e. { A , B } )
12 biid 
 |-  ( ( A e. V /\ A C_ B ) <-> ( A e. V /\ A C_ B ) )
13 12 bianass 
 |-  ( ( B e. _V /\ ( A e. V /\ A C_ B ) ) <-> ( ( B e. _V /\ A e. V ) /\ A C_ B ) )
14 inteq 
 |-  ( x = { A } -> |^| x = |^| { A } )
15 intsng 
 |-  ( A e. V -> |^| { A } = A )
16 15 adantl 
 |-  ( ( B e. _V /\ A e. V ) -> |^| { A } = A )
17 14 16 sylan9eqr 
 |-  ( ( ( B e. _V /\ A e. V ) /\ x = { A } ) -> |^| x = A )
18 prid1g 
 |-  ( A e. V -> A e. { A , B } )
19 18 adantl 
 |-  ( ( B e. _V /\ A e. V ) -> A e. { A , B } )
20 19 adantr 
 |-  ( ( ( B e. _V /\ A e. V ) /\ x = { A } ) -> A e. { A , B } )
21 17 20 eqeltrd 
 |-  ( ( ( B e. _V /\ A e. V ) /\ x = { A } ) -> |^| x e. { A , B } )
22 21 ex 
 |-  ( ( B e. _V /\ A e. V ) -> ( x = { A } -> |^| x e. { A , B } ) )
23 22 adantr 
 |-  ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) -> ( x = { A } -> |^| x e. { A , B } ) )
24 inteq 
 |-  ( x = { B } -> |^| x = |^| { B } )
25 intsng 
 |-  ( B e. _V -> |^| { B } = B )
26 25 adantr 
 |-  ( ( B e. _V /\ A e. V ) -> |^| { B } = B )
27 24 26 sylan9eqr 
 |-  ( ( ( B e. _V /\ A e. V ) /\ x = { B } ) -> |^| x = B )
28 9 ad2antrr 
 |-  ( ( ( B e. _V /\ A e. V ) /\ x = { B } ) -> B e. { A , B } )
29 27 28 eqeltrd 
 |-  ( ( ( B e. _V /\ A e. V ) /\ x = { B } ) -> |^| x e. { A , B } )
30 29 ex 
 |-  ( ( B e. _V /\ A e. V ) -> ( x = { B } -> |^| x e. { A , B } ) )
31 30 adantr 
 |-  ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) -> ( x = { B } -> |^| x e. { A , B } ) )
32 inteq 
 |-  ( x = { A , B } -> |^| x = |^| { A , B } )
33 32 adantl 
 |-  ( ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) /\ x = { A , B } ) -> |^| x = |^| { A , B } )
34 1 ad2antrr 
 |-  ( ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) /\ x = { A , B } ) -> ( A e. V /\ B e. _V ) )
35 intprg 
 |-  ( ( A e. V /\ B e. _V ) -> |^| { A , B } = ( A i^i B ) )
36 34 35 syl 
 |-  ( ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) /\ x = { A , B } ) -> |^| { A , B } = ( A i^i B ) )
37 dfss2 
 |-  ( A C_ B <-> ( A i^i B ) = A )
38 37 biimpi 
 |-  ( A C_ B -> ( A i^i B ) = A )
39 38 adantl 
 |-  ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) -> ( A i^i B ) = A )
40 39 adantr 
 |-  ( ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) /\ x = { A , B } ) -> ( A i^i B ) = A )
41 33 36 40 3eqtrd 
 |-  ( ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) /\ x = { A , B } ) -> |^| x = A )
42 18 ad3antlr 
 |-  ( ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) /\ x = { A , B } ) -> A e. { A , B } )
43 41 42 eqeltrd 
 |-  ( ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) /\ x = { A , B } ) -> |^| x e. { A , B } )
44 43 ex 
 |-  ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) -> ( x = { A , B } -> |^| x e. { A , B } ) )
45 31 44 jaod 
 |-  ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) -> ( ( x = { B } \/ x = { A , B } ) -> |^| x e. { A , B } ) )
46 23 45 jaod 
 |-  ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) -> ( ( x = { A } \/ ( x = { B } \/ x = { A , B } ) ) -> |^| x e. { A , B } ) )
47 sspr 
 |-  ( x C_ { A , B } <-> ( ( x = (/) \/ x = { A } ) \/ ( x = { B } \/ x = { A , B } ) ) )
48 andir 
 |-  ( ( ( ( x = (/) \/ x = { A } ) \/ ( x = { B } \/ x = { A , B } ) ) /\ x =/= (/) ) <-> ( ( ( x = (/) \/ x = { A } ) /\ x =/= (/) ) \/ ( ( x = { B } \/ x = { A , B } ) /\ x =/= (/) ) ) )
49 andir 
 |-  ( ( ( x = (/) \/ x = { A } ) /\ x =/= (/) ) <-> ( ( x = (/) /\ x =/= (/) ) \/ ( x = { A } /\ x =/= (/) ) ) )
50 eqneqall 
 |-  ( x = (/) -> ( x =/= (/) -> F. ) )
51 50 imp 
 |-  ( ( x = (/) /\ x =/= (/) ) -> F. )
52 simpl 
 |-  ( ( x = { A } /\ x =/= (/) ) -> x = { A } )
53 51 52 orim12i 
 |-  ( ( ( x = (/) /\ x =/= (/) ) \/ ( x = { A } /\ x =/= (/) ) ) -> ( F. \/ x = { A } ) )
54 falim 
 |-  ( F. -> x = { A } )
55 54 bj-jaoi1 
 |-  ( ( F. \/ x = { A } ) -> x = { A } )
56 53 55 syl 
 |-  ( ( ( x = (/) /\ x =/= (/) ) \/ ( x = { A } /\ x =/= (/) ) ) -> x = { A } )
57 49 56 sylbi 
 |-  ( ( ( x = (/) \/ x = { A } ) /\ x =/= (/) ) -> x = { A } )
58 simpl 
 |-  ( ( ( x = { B } \/ x = { A , B } ) /\ x =/= (/) ) -> ( x = { B } \/ x = { A , B } ) )
59 57 58 orim12i 
 |-  ( ( ( ( x = (/) \/ x = { A } ) /\ x =/= (/) ) \/ ( ( x = { B } \/ x = { A , B } ) /\ x =/= (/) ) ) -> ( x = { A } \/ ( x = { B } \/ x = { A , B } ) ) )
60 48 59 sylbi 
 |-  ( ( ( ( x = (/) \/ x = { A } ) \/ ( x = { B } \/ x = { A , B } ) ) /\ x =/= (/) ) -> ( x = { A } \/ ( x = { B } \/ x = { A , B } ) ) )
61 47 60 sylanb 
 |-  ( ( x C_ { A , B } /\ x =/= (/) ) -> ( x = { A } \/ ( x = { B } \/ x = { A , B } ) ) )
62 46 61 impel 
 |-  ( ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) /\ ( x C_ { A , B } /\ x =/= (/) ) ) -> |^| x e. { A , B } )
63 13 62 sylanb 
 |-  ( ( ( B e. _V /\ ( A e. V /\ A C_ B ) ) /\ ( x C_ { A , B } /\ x =/= (/) ) ) -> |^| x e. { A , B } )
64 11 63 bj-ismooredr2 
 |-  ( ( B e. _V /\ ( A e. V /\ A C_ B ) ) -> { A , B } e. Moore_ )
65 pm3.22 
 |-  ( ( -. B e. _V /\ A e. V ) -> ( A e. V /\ -. B e. _V ) )
66 65 adantrr 
 |-  ( ( -. B e. _V /\ ( A e. V /\ A C_ B ) ) -> ( A e. V /\ -. B e. _V ) )
67 prprc2 
 |-  ( -. B e. _V -> { A , B } = { A } )
68 67 adantl 
 |-  ( ( A e. V /\ -. B e. _V ) -> { A , B } = { A } )
69 68 eqcomd 
 |-  ( ( A e. V /\ -. B e. _V ) -> { A } = { A , B } )
70 66 69 syl 
 |-  ( ( -. B e. _V /\ ( A e. V /\ A C_ B ) ) -> { A } = { A , B } )
71 bj-snmoore 
 |-  ( A e. V -> { A } e. Moore_ )
72 71 ad2antrl 
 |-  ( ( -. B e. _V /\ ( A e. V /\ A C_ B ) ) -> { A } e. Moore_ )
73 70 72 eqeltrrd 
 |-  ( ( -. B e. _V /\ ( A e. V /\ A C_ B ) ) -> { A , B } e. Moore_ )
74 64 73 pm2.61ian 
 |-  ( ( A e. V /\ A C_ B ) -> { A , B } e. Moore_ )