Theorem clsk1indlem1

Description: The ansatz closure function ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) does not have the K1 property of isotony. (Contributed by RP, 6-Jul-2021)

	Ref	Expression
Hypothesis	clsk1indlem.k	⊢ 𝐾 = ( 𝑟 ∈ 𝒫 3o ↦ if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) )
Assertion	clsk1indlem1	⊢ ∃ 𝑠 ∈ 𝒫 3o ∃ 𝑡 ∈ 𝒫 3o ( 𝑠 ⊆ 𝑡 ∧ ¬ ( 𝐾 ‘ 𝑠 ) ⊆ ( 𝐾 ‘ 𝑡 ) )

Proof

Step	Hyp	Ref	Expression
1		clsk1indlem.k	⊢ 𝐾 = ( 𝑟 ∈ 𝒫 3o ↦ if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) )
2		tpex	⊢ { ∅ , 1o , 2o } ∈ V
3		snsstp1	⊢ { ∅ } ⊆ { ∅ , 1o , 2o }
4	2 3	elpwi2	⊢ { ∅ } ∈ 𝒫 { ∅ , 1o , 2o }
5		df3o2	⊢ 3o = { ∅ , 1o , 2o }
6	5	pweqi	⊢ 𝒫 3o = 𝒫 { ∅ , 1o , 2o }
7	4 6	eleqtrri	⊢ { ∅ } ∈ 𝒫 3o
8	2	a1i	⊢ ( ⊤ → { ∅ , 1o , 2o } ∈ V )
9	3	a1i	⊢ ( ⊤ → { ∅ } ⊆ { ∅ , 1o , 2o } )
10		0ex	⊢ ∅ ∈ V
11	10	snss	⊢ ( ∅ ∈ { ∅ , 1o , 2o } ↔ { ∅ } ⊆ { ∅ , 1o , 2o } )
12	9 11	sylibr	⊢ ( ⊤ → ∅ ∈ { ∅ , 1o , 2o } )
13		snsstp3	⊢ { 2o } ⊆ { ∅ , 1o , 2o }
14	13	a1i	⊢ ( ⊤ → { 2o } ⊆ { ∅ , 1o , 2o } )
15		2oex	⊢ 2o ∈ V
16	15	snss	⊢ ( 2o ∈ { ∅ , 1o , 2o } ↔ { 2o } ⊆ { ∅ , 1o , 2o } )
17	14 16	sylibr	⊢ ( ⊤ → 2o ∈ { ∅ , 1o , 2o } )
18	12 17	prssd	⊢ ( ⊤ → { ∅ , 2o } ⊆ { ∅ , 1o , 2o } )
19	8 18	sselpwd	⊢ ( ⊤ → { ∅ , 2o } ∈ 𝒫 { ∅ , 1o , 2o } )
20	19	mptru	⊢ { ∅ , 2o } ∈ 𝒫 { ∅ , 1o , 2o }
21	20 6	eleqtrri	⊢ { ∅ , 2o } ∈ 𝒫 3o
22		simpl	⊢ ( ( { ∅ } ∈ 𝒫 3o ∧ { ∅ , 2o } ∈ 𝒫 3o ) → { ∅ } ∈ 𝒫 3o )
23		sseq1	⊢ ( 𝑠 = { ∅ } → ( 𝑠 ⊆ 𝑡 ↔ { ∅ } ⊆ 𝑡 ) )
24		fveq2	⊢ ( 𝑠 = { ∅ } → ( 𝐾 ‘ 𝑠 ) = ( 𝐾 ‘ { ∅ } ) )
25	24	sseq1d	⊢ ( 𝑠 = { ∅ } → ( ( 𝐾 ‘ 𝑠 ) ⊆ ( 𝐾 ‘ 𝑡 ) ↔ ( 𝐾 ‘ { ∅ } ) ⊆ ( 𝐾 ‘ 𝑡 ) ) )
26	25	notbid	⊢ ( 𝑠 = { ∅ } → ( ¬ ( 𝐾 ‘ 𝑠 ) ⊆ ( 𝐾 ‘ 𝑡 ) ↔ ¬ ( 𝐾 ‘ { ∅ } ) ⊆ ( 𝐾 ‘ 𝑡 ) ) )
27	23 26	anbi12d	⊢ ( 𝑠 = { ∅ } → ( ( 𝑠 ⊆ 𝑡 ∧ ¬ ( 𝐾 ‘ 𝑠 ) ⊆ ( 𝐾 ‘ 𝑡 ) ) ↔ ( { ∅ } ⊆ 𝑡 ∧ ¬ ( 𝐾 ‘ { ∅ } ) ⊆ ( 𝐾 ‘ 𝑡 ) ) ) )
28	27	rexbidv	⊢ ( 𝑠 = { ∅ } → ( ∃ 𝑡 ∈ 𝒫 3o ( 𝑠 ⊆ 𝑡 ∧ ¬ ( 𝐾 ‘ 𝑠 ) ⊆ ( 𝐾 ‘ 𝑡 ) ) ↔ ∃ 𝑡 ∈ 𝒫 3o ( { ∅ } ⊆ 𝑡 ∧ ¬ ( 𝐾 ‘ { ∅ } ) ⊆ ( 𝐾 ‘ 𝑡 ) ) ) )
29	28	adantl	⊢ ( ( ( { ∅ } ∈ 𝒫 3o ∧ { ∅ , 2o } ∈ 𝒫 3o ) ∧ 𝑠 = { ∅ } ) → ( ∃ 𝑡 ∈ 𝒫 3o ( 𝑠 ⊆ 𝑡 ∧ ¬ ( 𝐾 ‘ 𝑠 ) ⊆ ( 𝐾 ‘ 𝑡 ) ) ↔ ∃ 𝑡 ∈ 𝒫 3o ( { ∅ } ⊆ 𝑡 ∧ ¬ ( 𝐾 ‘ { ∅ } ) ⊆ ( 𝐾 ‘ 𝑡 ) ) ) )
30		simpr	⊢ ( ( { ∅ } ∈ 𝒫 3o ∧ { ∅ , 2o } ∈ 𝒫 3o ) → { ∅ , 2o } ∈ 𝒫 3o )
31		fveq2	⊢ ( 𝑡 = { ∅ , 2o } → ( 𝐾 ‘ 𝑡 ) = ( 𝐾 ‘ { ∅ , 2o } ) )
32	31	sseq2d	⊢ ( 𝑡 = { ∅ , 2o } → ( ( 𝐾 ‘ { ∅ } ) ⊆ ( 𝐾 ‘ 𝑡 ) ↔ ( 𝐾 ‘ { ∅ } ) ⊆ ( 𝐾 ‘ { ∅ , 2o } ) ) )
33	32	notbid	⊢ ( 𝑡 = { ∅ , 2o } → ( ¬ ( 𝐾 ‘ { ∅ } ) ⊆ ( 𝐾 ‘ 𝑡 ) ↔ ¬ ( 𝐾 ‘ { ∅ } ) ⊆ ( 𝐾 ‘ { ∅ , 2o } ) ) )
34	33	cleq2lem	⊢ ( 𝑡 = { ∅ , 2o } → ( ( { ∅ } ⊆ 𝑡 ∧ ¬ ( 𝐾 ‘ { ∅ } ) ⊆ ( 𝐾 ‘ 𝑡 ) ) ↔ ( { ∅ } ⊆ { ∅ , 2o } ∧ ¬ ( 𝐾 ‘ { ∅ } ) ⊆ ( 𝐾 ‘ { ∅ , 2o } ) ) ) )
35	34	adantl	⊢ ( ( ( { ∅ } ∈ 𝒫 3o ∧ { ∅ , 2o } ∈ 𝒫 3o ) ∧ 𝑡 = { ∅ , 2o } ) → ( ( { ∅ } ⊆ 𝑡 ∧ ¬ ( 𝐾 ‘ { ∅ } ) ⊆ ( 𝐾 ‘ 𝑡 ) ) ↔ ( { ∅ } ⊆ { ∅ , 2o } ∧ ¬ ( 𝐾 ‘ { ∅ } ) ⊆ ( 𝐾 ‘ { ∅ , 2o } ) ) ) )
36		1oex	⊢ 1o ∈ V
37	36	prid2	⊢ 1o ∈ { ∅ , 1o }
38		iftrue	⊢ ( 𝑟 = { ∅ } → if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) = { ∅ , 1o } )
39		prex	⊢ { ∅ , 1o } ∈ V
40	38 1 39	fvmpt	⊢ ( { ∅ } ∈ 𝒫 3o → ( 𝐾 ‘ { ∅ } ) = { ∅ , 1o } )
41	40	adantr	⊢ ( ( { ∅ } ∈ 𝒫 3o ∧ { ∅ , 2o } ∈ 𝒫 3o ) → ( 𝐾 ‘ { ∅ } ) = { ∅ , 1o } )
42	37 41	eleqtrrid	⊢ ( ( { ∅ } ∈ 𝒫 3o ∧ { ∅ , 2o } ∈ 𝒫 3o ) → 1o ∈ ( 𝐾 ‘ { ∅ } ) )
43		1n0	⊢ 1o ≠ ∅
44	43	neii	⊢ ¬ 1o = ∅
45		eqcom	⊢ ( 1o = 2o ↔ 2o = 1o )
46		df-2o	⊢ 2o = suc 1o
47		df-1o	⊢ 1o = suc ∅
48	46 47	eqeq12i	⊢ ( 2o = 1o ↔ suc 1o = suc ∅ )
49		suc11reg	⊢ ( suc 1o = suc ∅ ↔ 1o = ∅ )
50	45 48 49	3bitri	⊢ ( 1o = 2o ↔ 1o = ∅ )
51	43 50	nemtbir	⊢ ¬ 1o = 2o
52	44 51	pm3.2ni	⊢ ¬ ( 1o = ∅ ∨ 1o = 2o )
53		elpri	⊢ ( 1o ∈ { ∅ , 2o } → ( 1o = ∅ ∨ 1o = 2o ) )
54	52 53	mto	⊢ ¬ 1o ∈ { ∅ , 2o }
55	54	a1i	⊢ ( ( { ∅ } ∈ 𝒫 3o ∧ { ∅ , 2o } ∈ 𝒫 3o ) → ¬ 1o ∈ { ∅ , 2o } )
56		eqeq1	⊢ ( 𝑟 = { ∅ , 2o } → ( 𝑟 = { ∅ } ↔ { ∅ , 2o } = { ∅ } ) )
57		id	⊢ ( 𝑟 = { ∅ , 2o } → 𝑟 = { ∅ , 2o } )
58	56 57	ifbieq2d	⊢ ( 𝑟 = { ∅ , 2o } → if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) = if ( { ∅ , 2o } = { ∅ } , { ∅ , 1o } , { ∅ , 2o } ) )
59	15	prid2	⊢ 2o ∈ { ∅ , 2o }
60		2on0	⊢ 2o ≠ ∅
61		nelsn	⊢ ( 2o ≠ ∅ → ¬ 2o ∈ { ∅ } )
62	60 61	ax-mp	⊢ ¬ 2o ∈ { ∅ }
63		nelneq2	⊢ ( ( 2o ∈ { ∅ , 2o } ∧ ¬ 2o ∈ { ∅ } ) → ¬ { ∅ , 2o } = { ∅ } )
64	59 62 63	mp2an	⊢ ¬ { ∅ , 2o } = { ∅ }
65	64	iffalsei	⊢ if ( { ∅ , 2o } = { ∅ } , { ∅ , 1o } , { ∅ , 2o } ) = { ∅ , 2o }
66	58 65	eqtrdi	⊢ ( 𝑟 = { ∅ , 2o } → if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) = { ∅ , 2o } )
67		prex	⊢ { ∅ , 2o } ∈ V
68	66 1 67	fvmpt	⊢ ( { ∅ , 2o } ∈ 𝒫 3o → ( 𝐾 ‘ { ∅ , 2o } ) = { ∅ , 2o } )
69	68	adantl	⊢ ( ( { ∅ } ∈ 𝒫 3o ∧ { ∅ , 2o } ∈ 𝒫 3o ) → ( 𝐾 ‘ { ∅ , 2o } ) = { ∅ , 2o } )
70	55 69	neleqtrrd	⊢ ( ( { ∅ } ∈ 𝒫 3o ∧ { ∅ , 2o } ∈ 𝒫 3o ) → ¬ 1o ∈ ( 𝐾 ‘ { ∅ , 2o } ) )
71		nelss	⊢ ( ( 1o ∈ ( 𝐾 ‘ { ∅ } ) ∧ ¬ 1o ∈ ( 𝐾 ‘ { ∅ , 2o } ) ) → ¬ ( 𝐾 ‘ { ∅ } ) ⊆ ( 𝐾 ‘ { ∅ , 2o } ) )
72	42 70 71	syl2anc	⊢ ( ( { ∅ } ∈ 𝒫 3o ∧ { ∅ , 2o } ∈ 𝒫 3o ) → ¬ ( 𝐾 ‘ { ∅ } ) ⊆ ( 𝐾 ‘ { ∅ , 2o } ) )
73		snsspr1	⊢ { ∅ } ⊆ { ∅ , 2o }
74	72 73	jctil	⊢ ( ( { ∅ } ∈ 𝒫 3o ∧ { ∅ , 2o } ∈ 𝒫 3o ) → ( { ∅ } ⊆ { ∅ , 2o } ∧ ¬ ( 𝐾 ‘ { ∅ } ) ⊆ ( 𝐾 ‘ { ∅ , 2o } ) ) )
75	30 35 74	rspcedvd	⊢ ( ( { ∅ } ∈ 𝒫 3o ∧ { ∅ , 2o } ∈ 𝒫 3o ) → ∃ 𝑡 ∈ 𝒫 3o ( { ∅ } ⊆ 𝑡 ∧ ¬ ( 𝐾 ‘ { ∅ } ) ⊆ ( 𝐾 ‘ 𝑡 ) ) )
76	22 29 75	rspcedvd	⊢ ( ( { ∅ } ∈ 𝒫 3o ∧ { ∅ , 2o } ∈ 𝒫 3o ) → ∃ 𝑠 ∈ 𝒫 3o ∃ 𝑡 ∈ 𝒫 3o ( 𝑠 ⊆ 𝑡 ∧ ¬ ( 𝐾 ‘ 𝑠 ) ⊆ ( 𝐾 ‘ 𝑡 ) ) )
77	7 21 76	mp2an	⊢ ∃ 𝑠 ∈ 𝒫 3o ∃ 𝑡 ∈ 𝒫 3o ( 𝑠 ⊆ 𝑡 ∧ ¬ ( 𝐾 ‘ 𝑠 ) ⊆ ( 𝐾 ‘ 𝑡 ) )