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	bilani	|- ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) -> ( A i^i B ) = A )
39	38	adantr	|- ( ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) /\ x = { A , B } ) -> ( A i^i B ) = A )
40	33 36 39	3eqtrd	|- ( ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) /\ x = { A , B } ) -> |^| x = A )
41	18	ad3antlr	|- ( ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) /\ x = { A , B } ) -> A e. { A , B } )
42	40 41	eqeltrd	|- ( ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) /\ x = { A , B } ) -> |^| x e. { A , B } )
43	42	ex	|- ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) -> ( x = { A , B } -> |^| x e. { A , B } ) )
44	31 43	jaod	|- ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) -> ( ( x = { B } \/ x = { A , B } ) -> |^| x e. { A , B } ) )
45	23 44	jaod	|- ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) -> ( ( x = { A } \/ ( x = { B } \/ x = { A , B } ) ) -> |^| x e. { A , B } ) )
46		sspr	|- ( x C_ { A , B } <-> ( ( x = (/) \/ x = { A } ) \/ ( x = { B } \/ x = { A , B } ) ) )
47		andir	|- ( ( ( ( x = (/) \/ x = { A } ) \/ ( x = { B } \/ x = { A , B } ) ) /\ x =/= (/) ) <-> ( ( ( x = (/) \/ x = { A } ) /\ x =/= (/) ) \/ ( ( x = { B } \/ x = { A , B } ) /\ x =/= (/) ) ) )
48		andir	|- ( ( ( x = (/) \/ x = { A } ) /\ x =/= (/) ) <-> ( ( x = (/) /\ x =/= (/) ) \/ ( x = { A } /\ x =/= (/) ) ) )
49		eqneqall	|- ( x = (/) -> ( x =/= (/) -> F. ) )
50	49	imp	|- ( ( x = (/) /\ x =/= (/) ) -> F. )
51		simpl	|- ( ( x = { A } /\ x =/= (/) ) -> x = { A } )
52	50 51	orim12i	|- ( ( ( x = (/) /\ x =/= (/) ) \/ ( x = { A } /\ x =/= (/) ) ) -> ( F. \/ x = { A } ) )
53		falim	|- ( F. -> x = { A } )
54	53	bj-jaoi1	|- ( ( F. \/ x = { A } ) -> x = { A } )
55	52 54	syl	|- ( ( ( x = (/) /\ x =/= (/) ) \/ ( x = { A } /\ x =/= (/) ) ) -> x = { A } )
56	48 55	sylbi	|- ( ( ( x = (/) \/ x = { A } ) /\ x =/= (/) ) -> x = { A } )
57		simpl	|- ( ( ( x = { B } \/ x = { A , B } ) /\ x =/= (/) ) -> ( x = { B } \/ x = { A , B } ) )
58	56 57	orim12i	|- ( ( ( ( x = (/) \/ x = { A } ) /\ x =/= (/) ) \/ ( ( x = { B } \/ x = { A , B } ) /\ x =/= (/) ) ) -> ( x = { A } \/ ( x = { B } \/ x = { A , B } ) ) )
59	47 58	sylbi	|- ( ( ( ( x = (/) \/ x = { A } ) \/ ( x = { B } \/ x = { A , B } ) ) /\ x =/= (/) ) -> ( x = { A } \/ ( x = { B } \/ x = { A , B } ) ) )
60	46 59	sylanb	|- ( ( x C_ { A , B } /\ x =/= (/) ) -> ( x = { A } \/ ( x = { B } \/ x = { A , B } ) ) )
61	45 60	impel	|- ( ( ( ( B e. _V /\ A e. V ) /\ A C_ B ) /\ ( x C_ { A , B } /\ x =/= (/) ) ) -> |^| x e. { A , B } )
62	13 61	sylanb	|- ( ( ( B e. _V /\ ( A e. V /\ A C_ B ) ) /\ ( x C_ { A , B } /\ x =/= (/) ) ) -> |^| x e. { A , B } )
63	11 62	bj-ismooredr2	|- ( ( B e. _V /\ ( A e. V /\ A C_ B ) ) -> { A , B } e. Moore_ )
64		pm3.22	|- ( ( -. B e. _V /\ A e. V ) -> ( A e. V /\ -. B e. _V ) )
65	64	adantrr	|- ( ( -. B e. _V /\ ( A e. V /\ A C_ B ) ) -> ( A e. V /\ -. B e. _V ) )
66		prprc2	|- ( -. B e. _V -> { A , B } = { A } )
67	66	adantl	|- ( ( A e. V /\ -. B e. _V ) -> { A , B } = { A } )
68	67	eqcomd	|- ( ( A e. V /\ -. B e. _V ) -> { A } = { A , B } )
69	65 68	syl	|- ( ( -. B e. _V /\ ( A e. V /\ A C_ B ) ) -> { A } = { A , B } )
70		bj-snmoore	|- ( A e. V -> { A } e. Moore_ )
71	70	ad2antrl	|- ( ( -. B e. _V /\ ( A e. V /\ A C_ B ) ) -> { A } e. Moore_ )
72	69 71	eqeltrrd	|- ( ( -. B e. _V /\ ( A e. V /\ A C_ B ) ) -> { A , B } e. Moore_ )
73	63 72	pm2.61ian	|- ( ( A e. V /\ A C_ B ) -> { A , B } e. Moore_ )