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		df-ss	|- ( 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_ )