Theorem isotone1 44066

Description: Two different ways to say subset relation persists across applications of a function. (Contributed by RP, 31-May-2021.)

Assertion

Ref	Expression
isotone1	⊢ (∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴(𝑎 ⊆ 𝑏 → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) ↔ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))

Distinct variable groups:   𝐴,𝑎,𝑏   𝐹,𝑎,𝑏

Proof of Theorem isotone1

Dummy variables 𝑐 𝑑 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sseq1 4008	. . . 4 ⊢ (𝑎 = 𝑐 → (𝑎 ⊆ 𝑏 ↔ 𝑐 ⊆ 𝑏))
2		fveq2 6905	. . . . 5 ⊢ (𝑎 = 𝑐 → (𝐹‘𝑎) = (𝐹‘𝑐))
3	2	sseq1d 4014	. . . 4 ⊢ (𝑎 = 𝑐 → ((𝐹‘𝑎) ⊆ (𝐹‘𝑏) ↔ (𝐹‘𝑐) ⊆ (𝐹‘𝑏)))
4	1, 3	imbi12d 344	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 ⊆ 𝑏 → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) ↔ (𝑐 ⊆ 𝑏 → (𝐹‘𝑐) ⊆ (𝐹‘𝑏))))
5		sseq2 4009	. . . 4 ⊢ (𝑏 = 𝑑 → (𝑐 ⊆ 𝑏 ↔ 𝑐 ⊆ 𝑑))
6		fveq2 6905	. . . . 5 ⊢ (𝑏 = 𝑑 → (𝐹‘𝑏) = (𝐹‘𝑑))
7	6	sseq2d 4015	. . . 4 ⊢ (𝑏 = 𝑑 → ((𝐹‘𝑐) ⊆ (𝐹‘𝑏) ↔ (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
8	5, 7	imbi12d 344	. . 3 ⊢ (𝑏 = 𝑑 → ((𝑐 ⊆ 𝑏 → (𝐹‘𝑐) ⊆ (𝐹‘𝑏)) ↔ (𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑))))
9	4, 8	cbvral2vw 3240	. 2 ⊢ (∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴(𝑎 ⊆ 𝑏 → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) ↔ ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
10		ssun1 4177	. . . . . 6 ⊢ 𝑎 ⊆ (𝑎 ∪ 𝑏)
11		simprl 770	. . . . . . 7 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → 𝑎 ∈ 𝒫 𝐴)
12		pwuncl 7791	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) → (𝑎 ∪ 𝑏) ∈ 𝒫 𝐴)
13	12	adantl 481	. . . . . . 7 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝑎 ∪ 𝑏) ∈ 𝒫 𝐴)
14		simpl 482	. . . . . . 7 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
15		sseq1 4008	. . . . . . . . 9 ⊢ (𝑐 = 𝑎 → (𝑐 ⊆ 𝑑 ↔ 𝑎 ⊆ 𝑑))
16		fveq2 6905	. . . . . . . . . 10 ⊢ (𝑐 = 𝑎 → (𝐹‘𝑐) = (𝐹‘𝑎))
17	16	sseq1d 4014	. . . . . . . . 9 ⊢ (𝑐 = 𝑎 → ((𝐹‘𝑐) ⊆ (𝐹‘𝑑) ↔ (𝐹‘𝑎) ⊆ (𝐹‘𝑑)))
18	15, 17	imbi12d 344	. . . . . . . 8 ⊢ (𝑐 = 𝑎 → ((𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ↔ (𝑎 ⊆ 𝑑 → (𝐹‘𝑎) ⊆ (𝐹‘𝑑))))
19		sseq2 4009	. . . . . . . . 9 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → (𝑎 ⊆ 𝑑 ↔ 𝑎 ⊆ (𝑎 ∪ 𝑏)))
20		fveq2 6905	. . . . . . . . . 10 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → (𝐹‘𝑑) = (𝐹‘(𝑎 ∪ 𝑏)))
21	20	sseq2d 4015	. . . . . . . . 9 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → ((𝐹‘𝑎) ⊆ (𝐹‘𝑑) ↔ (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
22	19, 21	imbi12d 344	. . . . . . . 8 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → ((𝑎 ⊆ 𝑑 → (𝐹‘𝑎) ⊆ (𝐹‘𝑑)) ↔ (𝑎 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))))
23	18, 22	rspc2va 3633	. . . . . . 7 ⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ (𝑎 ∪ 𝑏) ∈ 𝒫 𝐴) ∧ ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑))) → (𝑎 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
24	11, 13, 14, 23	syl21anc 837	. . . . . 6 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝑎 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
25	10, 24	mpi 20	. . . . 5 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
26		ssun2 4178	. . . . . 6 ⊢ 𝑏 ⊆ (𝑎 ∪ 𝑏)
27		simprr 772	. . . . . . 7 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → 𝑏 ∈ 𝒫 𝐴)
28		sseq1 4008	. . . . . . . . 9 ⊢ (𝑐 = 𝑏 → (𝑐 ⊆ 𝑑 ↔ 𝑏 ⊆ 𝑑))
29		fveq2 6905	. . . . . . . . . 10 ⊢ (𝑐 = 𝑏 → (𝐹‘𝑐) = (𝐹‘𝑏))
30	29	sseq1d 4014	. . . . . . . . 9 ⊢ (𝑐 = 𝑏 → ((𝐹‘𝑐) ⊆ (𝐹‘𝑑) ↔ (𝐹‘𝑏) ⊆ (𝐹‘𝑑)))
31	28, 30	imbi12d 344	. . . . . . . 8 ⊢ (𝑐 = 𝑏 → ((𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ↔ (𝑏 ⊆ 𝑑 → (𝐹‘𝑏) ⊆ (𝐹‘𝑑))))
32		sseq2 4009	. . . . . . . . 9 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → (𝑏 ⊆ 𝑑 ↔ 𝑏 ⊆ (𝑎 ∪ 𝑏)))
33	20	sseq2d 4015	. . . . . . . . 9 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → ((𝐹‘𝑏) ⊆ (𝐹‘𝑑) ↔ (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
34	32, 33	imbi12d 344	. . . . . . . 8 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → ((𝑏 ⊆ 𝑑 → (𝐹‘𝑏) ⊆ (𝐹‘𝑑)) ↔ (𝑏 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))))
35	31, 34	rspc2va 3633	. . . . . . 7 ⊢ (((𝑏 ∈ 𝒫 𝐴 ∧ (𝑎 ∪ 𝑏) ∈ 𝒫 𝐴) ∧ ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑))) → (𝑏 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
36	27, 13, 14, 35	syl21anc 837	. . . . . 6 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝑏 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
37	26, 36	mpi 20	. . . . 5 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
38	25, 37	unssd 4191	. . . 4 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
39	38	ralrimivva 3201	. . 3 ⊢ (∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) → ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
40		ssequn1 4185	. . . . 5 ⊢ (𝑐 ⊆ 𝑑 ↔ (𝑐 ∪ 𝑑) = 𝑑)
41	2	uneq1d 4166	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) = ((𝐹‘𝑐) ∪ (𝐹‘𝑏)))
42		uneq1 4160	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝑎 ∪ 𝑏) = (𝑐 ∪ 𝑏))
43	42	fveq2d 6909	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (𝐹‘(𝑎 ∪ 𝑏)) = (𝐹‘(𝑐 ∪ 𝑏)))
44	41, 43	sseq12d 4016	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑐 → (((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ↔ ((𝐹‘𝑐) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑐 ∪ 𝑏))))
45	6	uneq2d 4167	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → ((𝐹‘𝑐) ∪ (𝐹‘𝑏)) = ((𝐹‘𝑐) ∪ (𝐹‘𝑑)))
46		uneq2 4161	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑑 → (𝑐 ∪ 𝑏) = (𝑐 ∪ 𝑑))
47	46	fveq2d 6909	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (𝐹‘(𝑐 ∪ 𝑏)) = (𝐹‘(𝑐 ∪ 𝑑)))
48	45, 47	sseq12d 4016	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑑 → (((𝐹‘𝑐) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑐 ∪ 𝑏)) ↔ ((𝐹‘𝑐) ∪ (𝐹‘𝑑)) ⊆ (𝐹‘(𝑐 ∪ 𝑑))))
49	44, 48	rspc2va 3633	. . . . . . . . . 10 ⊢ (((𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴) ∧ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏))) → ((𝐹‘𝑐) ∪ (𝐹‘𝑑)) ⊆ (𝐹‘(𝑐 ∪ 𝑑)))
50	49	ancoms 458	. . . . . . . . 9 ⊢ ((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) → ((𝐹‘𝑐) ∪ (𝐹‘𝑑)) ⊆ (𝐹‘(𝑐 ∪ 𝑑)))
51	50	unssad 4192	. . . . . . . 8 ⊢ ((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) → (𝐹‘𝑐) ⊆ (𝐹‘(𝑐 ∪ 𝑑)))
52	51	adantr 480	. . . . . . 7 ⊢ (((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐 ∪ 𝑑) = 𝑑) → (𝐹‘𝑐) ⊆ (𝐹‘(𝑐 ∪ 𝑑)))
53		fveq2 6905	. . . . . . . 8 ⊢ ((𝑐 ∪ 𝑑) = 𝑑 → (𝐹‘(𝑐 ∪ 𝑑)) = (𝐹‘𝑑))
54	53	adantl 481	. . . . . . 7 ⊢ (((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐 ∪ 𝑑) = 𝑑) → (𝐹‘(𝑐 ∪ 𝑑)) = (𝐹‘𝑑))
55	52, 54	sseqtrd 4019	. . . . . 6 ⊢ (((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐 ∪ 𝑑) = 𝑑) → (𝐹‘𝑐) ⊆ (𝐹‘𝑑))
56	55	ex 412	. . . . 5 ⊢ ((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) → ((𝑐 ∪ 𝑑) = 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
57	40, 56	biimtrid 242	. . . 4 ⊢ ((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) → (𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
58	57	ralrimivva 3201	. . 3 ⊢ (∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) → ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
59	39, 58	impbii 209	. 2 ⊢ (∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ↔ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
60	9, 59	bitri 275	1 ⊢ (∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴(𝑎 ⊆ 𝑏 → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) ↔ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ∀wral 3060   ∪ cun 3948   ⊆ wss 3950  𝒫 cpw 4599  ‘cfv 6560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431  ax-un 7756

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-iota 6513  df-fv 6568

This theorem is referenced by: (None)