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		1oelpr	⊢ 1o ∈ { ∅ , 1o }
37		iftrue	⊢ ( 𝑟 = { ∅ } → if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) = { ∅ , 1o } )
38		prex	⊢ { ∅ , 1o } ∈ V
39	37 1 38	fvmpt	⊢ ( { ∅ } ∈ 𝒫 3o → ( 𝐾 ‘ { ∅ } ) = { ∅ , 1o } )
40	39	adantr	⊢ ( ( { ∅ } ∈ 𝒫 3o ∧ { ∅ , 2o } ∈ 𝒫 3o ) → ( 𝐾 ‘ { ∅ } ) = { ∅ , 1o } )
41	36 40	eleqtrrid	⊢ ( ( { ∅ } ∈ 𝒫 3o ∧ { ∅ , 2o } ∈ 𝒫 3o ) → 1o ∈ ( 𝐾 ‘ { ∅ } ) )
42		1n0	⊢ 1o ≠ ∅
43	42	neii	⊢ ¬ 1o = ∅
44		eqcom	⊢ ( 1o = 2o ↔ 2o = 1o )
45		df-2o	⊢ 2o = suc 1o
46		df-1o	⊢ 1o = suc ∅
47	45 46	eqeq12i	⊢ ( 2o = 1o ↔ suc 1o = suc ∅ )
48		suc11reg	⊢ ( suc 1o = suc ∅ ↔ 1o = ∅ )
49	44 47 48	3bitri	⊢ ( 1o = 2o ↔ 1o = ∅ )
50	42 49	nemtbir	⊢ ¬ 1o = 2o
51	43 50	pm3.2ni	⊢ ¬ ( 1o = ∅ ∨ 1o = 2o )
52		elpri	⊢ ( 1o ∈ { ∅ , 2o } → ( 1o = ∅ ∨ 1o = 2o ) )
53	51 52	mto	⊢ ¬ 1o ∈ { ∅ , 2o }
54	53	a1i	⊢ ( ( { ∅ } ∈ 𝒫 3o ∧ { ∅ , 2o } ∈ 𝒫 3o ) → ¬ 1o ∈ { ∅ , 2o } )
55		eqeq1	⊢ ( 𝑟 = { ∅ , 2o } → ( 𝑟 = { ∅ } ↔ { ∅ , 2o } = { ∅ } ) )
56		id	⊢ ( 𝑟 = { ∅ , 2o } → 𝑟 = { ∅ , 2o } )
57	55 56	ifbieq2d	⊢ ( 𝑟 = { ∅ , 2o } → if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) = if ( { ∅ , 2o } = { ∅ } , { ∅ , 1o } , { ∅ , 2o } ) )
58	15	prid2	⊢ 2o ∈ { ∅ , 2o }
59		2on0	⊢ 2o ≠ ∅
60		nelsn	⊢ ( 2o ≠ ∅ → ¬ 2o ∈ { ∅ } )
61	59 60	ax-mp	⊢ ¬ 2o ∈ { ∅ }
62		nelneq2	⊢ ( ( 2o ∈ { ∅ , 2o } ∧ ¬ 2o ∈ { ∅ } ) → ¬ { ∅ , 2o } = { ∅ } )
63	58 61 62	mp2an	⊢ ¬ { ∅ , 2o } = { ∅ }
64	63	iffalsei	⊢ if ( { ∅ , 2o } = { ∅ } , { ∅ , 1o } , { ∅ , 2o } ) = { ∅ , 2o }
65	57 64	eqtrdi	⊢ ( 𝑟 = { ∅ , 2o } → if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) = { ∅ , 2o } )
66		prex	⊢ { ∅ , 2o } ∈ V
67	65 1 66	fvmpt	⊢ ( { ∅ , 2o } ∈ 𝒫 3o → ( 𝐾 ‘ { ∅ , 2o } ) = { ∅ , 2o } )
68	67	adantl	⊢ ( ( { ∅ } ∈ 𝒫 3o ∧ { ∅ , 2o } ∈ 𝒫 3o ) → ( 𝐾 ‘ { ∅ , 2o } ) = { ∅ , 2o } )
69	54 68	neleqtrrd	⊢ ( ( { ∅ } ∈ 𝒫 3o ∧ { ∅ , 2o } ∈ 𝒫 3o ) → ¬ 1o ∈ ( 𝐾 ‘ { ∅ , 2o } ) )
70		nelss	⊢ ( ( 1o ∈ ( 𝐾 ‘ { ∅ } ) ∧ ¬ 1o ∈ ( 𝐾 ‘ { ∅ , 2o } ) ) → ¬ ( 𝐾 ‘ { ∅ } ) ⊆ ( 𝐾 ‘ { ∅ , 2o } ) )
71	41 69 70	syl2anc	⊢ ( ( { ∅ } ∈ 𝒫 3o ∧ { ∅ , 2o } ∈ 𝒫 3o ) → ¬ ( 𝐾 ‘ { ∅ } ) ⊆ ( 𝐾 ‘ { ∅ , 2o } ) )
72		snsspr1	⊢ { ∅ } ⊆ { ∅ , 2o }
73	71 72	jctil	⊢ ( ( { ∅ } ∈ 𝒫 3o ∧ { ∅ , 2o } ∈ 𝒫 3o ) → ( { ∅ } ⊆ { ∅ , 2o } ∧ ¬ ( 𝐾 ‘ { ∅ } ) ⊆ ( 𝐾 ‘ { ∅ , 2o } ) ) )
74	30 35 73	rspcedvd	⊢ ( ( { ∅ } ∈ 𝒫 3o ∧ { ∅ , 2o } ∈ 𝒫 3o ) → ∃ 𝑡 ∈ 𝒫 3o ( { ∅ } ⊆ 𝑡 ∧ ¬ ( 𝐾 ‘ { ∅ } ) ⊆ ( 𝐾 ‘ 𝑡 ) ) )
75	22 29 74	rspcedvd	⊢ ( ( { ∅ } ∈ 𝒫 3o ∧ { ∅ , 2o } ∈ 𝒫 3o ) → ∃ 𝑠 ∈ 𝒫 3o ∃ 𝑡 ∈ 𝒫 3o ( 𝑠 ⊆ 𝑡 ∧ ¬ ( 𝐾 ‘ 𝑠 ) ⊆ ( 𝐾 ‘ 𝑡 ) ) )
76	7 21 75	mp2an	⊢ ∃ 𝑠 ∈ 𝒫 3o ∃ 𝑡 ∈ 𝒫 3o ( 𝑠 ⊆ 𝑡 ∧ ¬ ( 𝐾 ‘ 𝑠 ) ⊆ ( 𝐾 ‘ 𝑡 ) )