Theorem isotone1 41124

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 3917	. . . 4 ⊢ (𝑎 = 𝑐 → (𝑎 ⊆ 𝑏 ↔ 𝑐 ⊆ 𝑏))
2		fveq2 6658	. . . . 5 ⊢ (𝑎 = 𝑐 → (𝐹‘𝑎) = (𝐹‘𝑐))
3	2	sseq1d 3923	. . . 4 ⊢ (𝑎 = 𝑐 → ((𝐹‘𝑎) ⊆ (𝐹‘𝑏) ↔ (𝐹‘𝑐) ⊆ (𝐹‘𝑏)))
4	1, 3	imbi12d 348	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 ⊆ 𝑏 → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) ↔ (𝑐 ⊆ 𝑏 → (𝐹‘𝑐) ⊆ (𝐹‘𝑏))))
5		sseq2 3918	. . . 4 ⊢ (𝑏 = 𝑑 → (𝑐 ⊆ 𝑏 ↔ 𝑐 ⊆ 𝑑))
6		fveq2 6658	. . . . 5 ⊢ (𝑏 = 𝑑 → (𝐹‘𝑏) = (𝐹‘𝑑))
7	6	sseq2d 3924	. . . 4 ⊢ (𝑏 = 𝑑 → ((𝐹‘𝑐) ⊆ (𝐹‘𝑏) ↔ (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
8	5, 7	imbi12d 348	. . 3 ⊢ (𝑏 = 𝑑 → ((𝑐 ⊆ 𝑏 → (𝐹‘𝑐) ⊆ (𝐹‘𝑏)) ↔ (𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑))))
9	4, 8	cbvral2vw 3373	. 2 ⊢ (∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴(𝑎 ⊆ 𝑏 → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) ↔ ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
10		ssun1 4077	. . . . . 6 ⊢ 𝑎 ⊆ (𝑎 ∪ 𝑏)
11		simprl 770	. . . . . . 7 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → 𝑎 ∈ 𝒫 𝐴)
12		pwuncl 7491	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) → (𝑎 ∪ 𝑏) ∈ 𝒫 𝐴)
13	12	adantl 485	. . . . . . 7 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝑎 ∪ 𝑏) ∈ 𝒫 𝐴)
14		simpl 486	. . . . . . 7 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
15		sseq1 3917	. . . . . . . . 9 ⊢ (𝑐 = 𝑎 → (𝑐 ⊆ 𝑑 ↔ 𝑎 ⊆ 𝑑))
16		fveq2 6658	. . . . . . . . . 10 ⊢ (𝑐 = 𝑎 → (𝐹‘𝑐) = (𝐹‘𝑎))
17	16	sseq1d 3923	. . . . . . . . 9 ⊢ (𝑐 = 𝑎 → ((𝐹‘𝑐) ⊆ (𝐹‘𝑑) ↔ (𝐹‘𝑎) ⊆ (𝐹‘𝑑)))
18	15, 17	imbi12d 348	. . . . . . . 8 ⊢ (𝑐 = 𝑎 → ((𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ↔ (𝑎 ⊆ 𝑑 → (𝐹‘𝑎) ⊆ (𝐹‘𝑑))))
19		sseq2 3918	. . . . . . . . 9 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → (𝑎 ⊆ 𝑑 ↔ 𝑎 ⊆ (𝑎 ∪ 𝑏)))
20		fveq2 6658	. . . . . . . . . 10 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → (𝐹‘𝑑) = (𝐹‘(𝑎 ∪ 𝑏)))
21	20	sseq2d 3924	. . . . . . . . 9 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → ((𝐹‘𝑎) ⊆ (𝐹‘𝑑) ↔ (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
22	19, 21	imbi12d 348	. . . . . . . 8 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → ((𝑎 ⊆ 𝑑 → (𝐹‘𝑎) ⊆ (𝐹‘𝑑)) ↔ (𝑎 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))))
23	18, 22	rspc2va 3552	. . . . . . 7 ⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ (𝑎 ∪ 𝑏) ∈ 𝒫 𝐴) ∧ ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑))) → (𝑎 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
24	11, 13, 14, 23	syl21anc 836	. . . . . 6 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝑎 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
25	10, 24	mpi 20	. . . . 5 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
26		ssun2 4078	. . . . . 6 ⊢ 𝑏 ⊆ (𝑎 ∪ 𝑏)
27		simprr 772	. . . . . . 7 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → 𝑏 ∈ 𝒫 𝐴)
28		sseq1 3917	. . . . . . . . 9 ⊢ (𝑐 = 𝑏 → (𝑐 ⊆ 𝑑 ↔ 𝑏 ⊆ 𝑑))
29		fveq2 6658	. . . . . . . . . 10 ⊢ (𝑐 = 𝑏 → (𝐹‘𝑐) = (𝐹‘𝑏))
30	29	sseq1d 3923	. . . . . . . . 9 ⊢ (𝑐 = 𝑏 → ((𝐹‘𝑐) ⊆ (𝐹‘𝑑) ↔ (𝐹‘𝑏) ⊆ (𝐹‘𝑑)))
31	28, 30	imbi12d 348	. . . . . . . 8 ⊢ (𝑐 = 𝑏 → ((𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ↔ (𝑏 ⊆ 𝑑 → (𝐹‘𝑏) ⊆ (𝐹‘𝑑))))
32		sseq2 3918	. . . . . . . . 9 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → (𝑏 ⊆ 𝑑 ↔ 𝑏 ⊆ (𝑎 ∪ 𝑏)))
33	20	sseq2d 3924	. . . . . . . . 9 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → ((𝐹‘𝑏) ⊆ (𝐹‘𝑑) ↔ (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
34	32, 33	imbi12d 348	. . . . . . . 8 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → ((𝑏 ⊆ 𝑑 → (𝐹‘𝑏) ⊆ (𝐹‘𝑑)) ↔ (𝑏 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))))
35	31, 34	rspc2va 3552	. . . . . . 7 ⊢ (((𝑏 ∈ 𝒫 𝐴 ∧ (𝑎 ∪ 𝑏) ∈ 𝒫 𝐴) ∧ ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑))) → (𝑏 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
36	27, 13, 14, 35	syl21anc 836	. . . . . 6 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝑏 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
37	26, 36	mpi 20	. . . . 5 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
38	25, 37	unssd 4091	. . . 4 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
39	38	ralrimivva 3120	. . 3 ⊢ (∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) → ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
40		ssequn1 4085	. . . . 5 ⊢ (𝑐 ⊆ 𝑑 ↔ (𝑐 ∪ 𝑑) = 𝑑)
41	2	uneq1d 4067	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) = ((𝐹‘𝑐) ∪ (𝐹‘𝑏)))
42		uneq1 4061	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝑎 ∪ 𝑏) = (𝑐 ∪ 𝑏))
43	42	fveq2d 6662	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (𝐹‘(𝑎 ∪ 𝑏)) = (𝐹‘(𝑐 ∪ 𝑏)))
44	41, 43	sseq12d 3925	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑐 → (((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ↔ ((𝐹‘𝑐) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑐 ∪ 𝑏))))
45	6	uneq2d 4068	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → ((𝐹‘𝑐) ∪ (𝐹‘𝑏)) = ((𝐹‘𝑐) ∪ (𝐹‘𝑑)))
46		uneq2 4062	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑑 → (𝑐 ∪ 𝑏) = (𝑐 ∪ 𝑑))
47	46	fveq2d 6662	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (𝐹‘(𝑐 ∪ 𝑏)) = (𝐹‘(𝑐 ∪ 𝑑)))
48	45, 47	sseq12d 3925	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑑 → (((𝐹‘𝑐) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑐 ∪ 𝑏)) ↔ ((𝐹‘𝑐) ∪ (𝐹‘𝑑)) ⊆ (𝐹‘(𝑐 ∪ 𝑑))))
49	44, 48	rspc2va 3552	. . . . . . . . . 10 ⊢ (((𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴) ∧ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏))) → ((𝐹‘𝑐) ∪ (𝐹‘𝑑)) ⊆ (𝐹‘(𝑐 ∪ 𝑑)))
50	49	ancoms 462	. . . . . . . . 9 ⊢ ((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) → ((𝐹‘𝑐) ∪ (𝐹‘𝑑)) ⊆ (𝐹‘(𝑐 ∪ 𝑑)))
51	50	unssad 4092	. . . . . . . 8 ⊢ ((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) → (𝐹‘𝑐) ⊆ (𝐹‘(𝑐 ∪ 𝑑)))
52	51	adantr 484	. . . . . . 7 ⊢ (((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐 ∪ 𝑑) = 𝑑) → (𝐹‘𝑐) ⊆ (𝐹‘(𝑐 ∪ 𝑑)))
53		fveq2 6658	. . . . . . . 8 ⊢ ((𝑐 ∪ 𝑑) = 𝑑 → (𝐹‘(𝑐 ∪ 𝑑)) = (𝐹‘𝑑))
54	53	adantl 485	. . . . . . 7 ⊢ (((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐 ∪ 𝑑) = 𝑑) → (𝐹‘(𝑐 ∪ 𝑑)) = (𝐹‘𝑑))
55	52, 54	sseqtrd 3932	. . . . . 6 ⊢ (((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐 ∪ 𝑑) = 𝑑) → (𝐹‘𝑐) ⊆ (𝐹‘𝑑))
56	55	ex 416	. . . . 5 ⊢ ((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) → ((𝑐 ∪ 𝑑) = 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
57	40, 56	syl5bi 245	. . . 4 ⊢ ((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) → (𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
58	57	ralrimivva 3120	. . 3 ⊢ (∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) → ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
59	39, 58	impbii 212	. 2 ⊢ (∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ↔ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
60	9, 59	bitri 278	1 ⊢ (∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴(𝑎 ⊆ 𝑏 → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) ↔ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3070   ∪ cun 3856   ⊆ wss 3858  𝒫 cpw 4494  ‘cfv 6335

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298  ax-un 7459

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ral 3075  df-rab 3079  df-v 3411  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-pw 4496  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-iota 6294  df-fv 6343

This theorem is referenced by: (None)