Theorem isotone1 41547

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 3942	. . . 4 ⊢ (𝑎 = 𝑐 → (𝑎 ⊆ 𝑏 ↔ 𝑐 ⊆ 𝑏))
2		fveq2 6756	. . . . 5 ⊢ (𝑎 = 𝑐 → (𝐹‘𝑎) = (𝐹‘𝑐))
3	2	sseq1d 3948	. . . 4 ⊢ (𝑎 = 𝑐 → ((𝐹‘𝑎) ⊆ (𝐹‘𝑏) ↔ (𝐹‘𝑐) ⊆ (𝐹‘𝑏)))
4	1, 3	imbi12d 344	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 ⊆ 𝑏 → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) ↔ (𝑐 ⊆ 𝑏 → (𝐹‘𝑐) ⊆ (𝐹‘𝑏))))
5		sseq2 3943	. . . 4 ⊢ (𝑏 = 𝑑 → (𝑐 ⊆ 𝑏 ↔ 𝑐 ⊆ 𝑑))
6		fveq2 6756	. . . . 5 ⊢ (𝑏 = 𝑑 → (𝐹‘𝑏) = (𝐹‘𝑑))
7	6	sseq2d 3949	. . . 4 ⊢ (𝑏 = 𝑑 → ((𝐹‘𝑐) ⊆ (𝐹‘𝑏) ↔ (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
8	5, 7	imbi12d 344	. . 3 ⊢ (𝑏 = 𝑑 → ((𝑐 ⊆ 𝑏 → (𝐹‘𝑐) ⊆ (𝐹‘𝑏)) ↔ (𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑))))
9	4, 8	cbvral2vw 3385	. 2 ⊢ (∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴(𝑎 ⊆ 𝑏 → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) ↔ ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
10		ssun1 4102	. . . . . 6 ⊢ 𝑎 ⊆ (𝑎 ∪ 𝑏)
11		simprl 767	. . . . . . 7 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → 𝑎 ∈ 𝒫 𝐴)
12		pwuncl 7598	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) → (𝑎 ∪ 𝑏) ∈ 𝒫 𝐴)
13	12	adantl 481	. . . . . . 7 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝑎 ∪ 𝑏) ∈ 𝒫 𝐴)
14		simpl 482	. . . . . . 7 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
15		sseq1 3942	. . . . . . . . 9 ⊢ (𝑐 = 𝑎 → (𝑐 ⊆ 𝑑 ↔ 𝑎 ⊆ 𝑑))
16		fveq2 6756	. . . . . . . . . 10 ⊢ (𝑐 = 𝑎 → (𝐹‘𝑐) = (𝐹‘𝑎))
17	16	sseq1d 3948	. . . . . . . . 9 ⊢ (𝑐 = 𝑎 → ((𝐹‘𝑐) ⊆ (𝐹‘𝑑) ↔ (𝐹‘𝑎) ⊆ (𝐹‘𝑑)))
18	15, 17	imbi12d 344	. . . . . . . 8 ⊢ (𝑐 = 𝑎 → ((𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ↔ (𝑎 ⊆ 𝑑 → (𝐹‘𝑎) ⊆ (𝐹‘𝑑))))
19		sseq2 3943	. . . . . . . . 9 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → (𝑎 ⊆ 𝑑 ↔ 𝑎 ⊆ (𝑎 ∪ 𝑏)))
20		fveq2 6756	. . . . . . . . . 10 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → (𝐹‘𝑑) = (𝐹‘(𝑎 ∪ 𝑏)))
21	20	sseq2d 3949	. . . . . . . . 9 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → ((𝐹‘𝑎) ⊆ (𝐹‘𝑑) ↔ (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
22	19, 21	imbi12d 344	. . . . . . . 8 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → ((𝑎 ⊆ 𝑑 → (𝐹‘𝑎) ⊆ (𝐹‘𝑑)) ↔ (𝑎 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))))
23	18, 22	rspc2va 3563	. . . . . . 7 ⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ (𝑎 ∪ 𝑏) ∈ 𝒫 𝐴) ∧ ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑))) → (𝑎 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
24	11, 13, 14, 23	syl21anc 834	. . . . . 6 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝑎 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
25	10, 24	mpi 20	. . . . 5 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
26		ssun2 4103	. . . . . 6 ⊢ 𝑏 ⊆ (𝑎 ∪ 𝑏)
27		simprr 769	. . . . . . 7 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → 𝑏 ∈ 𝒫 𝐴)
28		sseq1 3942	. . . . . . . . 9 ⊢ (𝑐 = 𝑏 → (𝑐 ⊆ 𝑑 ↔ 𝑏 ⊆ 𝑑))
29		fveq2 6756	. . . . . . . . . 10 ⊢ (𝑐 = 𝑏 → (𝐹‘𝑐) = (𝐹‘𝑏))
30	29	sseq1d 3948	. . . . . . . . 9 ⊢ (𝑐 = 𝑏 → ((𝐹‘𝑐) ⊆ (𝐹‘𝑑) ↔ (𝐹‘𝑏) ⊆ (𝐹‘𝑑)))
31	28, 30	imbi12d 344	. . . . . . . 8 ⊢ (𝑐 = 𝑏 → ((𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ↔ (𝑏 ⊆ 𝑑 → (𝐹‘𝑏) ⊆ (𝐹‘𝑑))))
32		sseq2 3943	. . . . . . . . 9 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → (𝑏 ⊆ 𝑑 ↔ 𝑏 ⊆ (𝑎 ∪ 𝑏)))
33	20	sseq2d 3949	. . . . . . . . 9 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → ((𝐹‘𝑏) ⊆ (𝐹‘𝑑) ↔ (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
34	32, 33	imbi12d 344	. . . . . . . 8 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → ((𝑏 ⊆ 𝑑 → (𝐹‘𝑏) ⊆ (𝐹‘𝑑)) ↔ (𝑏 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))))
35	31, 34	rspc2va 3563	. . . . . . 7 ⊢ (((𝑏 ∈ 𝒫 𝐴 ∧ (𝑎 ∪ 𝑏) ∈ 𝒫 𝐴) ∧ ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑))) → (𝑏 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
36	27, 13, 14, 35	syl21anc 834	. . . . . 6 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝑏 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
37	26, 36	mpi 20	. . . . 5 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
38	25, 37	unssd 4116	. . . 4 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
39	38	ralrimivva 3114	. . 3 ⊢ (∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) → ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
40		ssequn1 4110	. . . . 5 ⊢ (𝑐 ⊆ 𝑑 ↔ (𝑐 ∪ 𝑑) = 𝑑)
41	2	uneq1d 4092	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) = ((𝐹‘𝑐) ∪ (𝐹‘𝑏)))
42		uneq1 4086	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝑎 ∪ 𝑏) = (𝑐 ∪ 𝑏))
43	42	fveq2d 6760	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (𝐹‘(𝑎 ∪ 𝑏)) = (𝐹‘(𝑐 ∪ 𝑏)))
44	41, 43	sseq12d 3950	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑐 → (((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ↔ ((𝐹‘𝑐) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑐 ∪ 𝑏))))
45	6	uneq2d 4093	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → ((𝐹‘𝑐) ∪ (𝐹‘𝑏)) = ((𝐹‘𝑐) ∪ (𝐹‘𝑑)))
46		uneq2 4087	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑑 → (𝑐 ∪ 𝑏) = (𝑐 ∪ 𝑑))
47	46	fveq2d 6760	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (𝐹‘(𝑐 ∪ 𝑏)) = (𝐹‘(𝑐 ∪ 𝑑)))
48	45, 47	sseq12d 3950	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑑 → (((𝐹‘𝑐) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑐 ∪ 𝑏)) ↔ ((𝐹‘𝑐) ∪ (𝐹‘𝑑)) ⊆ (𝐹‘(𝑐 ∪ 𝑑))))
49	44, 48	rspc2va 3563	. . . . . . . . . 10 ⊢ (((𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴) ∧ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏))) → ((𝐹‘𝑐) ∪ (𝐹‘𝑑)) ⊆ (𝐹‘(𝑐 ∪ 𝑑)))
50	49	ancoms 458	. . . . . . . . 9 ⊢ ((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) → ((𝐹‘𝑐) ∪ (𝐹‘𝑑)) ⊆ (𝐹‘(𝑐 ∪ 𝑑)))
51	50	unssad 4117	. . . . . . . 8 ⊢ ((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) → (𝐹‘𝑐) ⊆ (𝐹‘(𝑐 ∪ 𝑑)))
52	51	adantr 480	. . . . . . 7 ⊢ (((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐 ∪ 𝑑) = 𝑑) → (𝐹‘𝑐) ⊆ (𝐹‘(𝑐 ∪ 𝑑)))
53		fveq2 6756	. . . . . . . 8 ⊢ ((𝑐 ∪ 𝑑) = 𝑑 → (𝐹‘(𝑐 ∪ 𝑑)) = (𝐹‘𝑑))
54	53	adantl 481	. . . . . . 7 ⊢ (((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐 ∪ 𝑑) = 𝑑) → (𝐹‘(𝑐 ∪ 𝑑)) = (𝐹‘𝑑))
55	52, 54	sseqtrd 3957	. . . . . 6 ⊢ (((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐 ∪ 𝑑) = 𝑑) → (𝐹‘𝑐) ⊆ (𝐹‘𝑑))
56	55	ex 412	. . . . 5 ⊢ ((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) → ((𝑐 ∪ 𝑑) = 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
57	40, 56	syl5bi 241	. . . 4 ⊢ ((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) → (𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
58	57	ralrimivva 3114	. . 3 ⊢ (∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) → ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
59	39, 58	impbii 208	. 2 ⊢ (∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ↔ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
60	9, 59	bitri 274	1 ⊢ (∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴(𝑎 ⊆ 𝑏 → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) ↔ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∀wral 3063   ∪ cun 3881   ⊆ wss 3883  𝒫 cpw 4530  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426

This theorem is referenced by: (None)