Theorem isotone1 40396

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 3991	. . . 4 ⊢ (𝑎 = 𝑐 → (𝑎 ⊆ 𝑏 ↔ 𝑐 ⊆ 𝑏))
2		fveq2 6669	. . . . 5 ⊢ (𝑎 = 𝑐 → (𝐹‘𝑎) = (𝐹‘𝑐))
3	2	sseq1d 3997	. . . 4 ⊢ (𝑎 = 𝑐 → ((𝐹‘𝑎) ⊆ (𝐹‘𝑏) ↔ (𝐹‘𝑐) ⊆ (𝐹‘𝑏)))
4	1, 3	imbi12d 347	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 ⊆ 𝑏 → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) ↔ (𝑐 ⊆ 𝑏 → (𝐹‘𝑐) ⊆ (𝐹‘𝑏))))
5		sseq2 3992	. . . 4 ⊢ (𝑏 = 𝑑 → (𝑐 ⊆ 𝑏 ↔ 𝑐 ⊆ 𝑑))
6		fveq2 6669	. . . . 5 ⊢ (𝑏 = 𝑑 → (𝐹‘𝑏) = (𝐹‘𝑑))
7	6	sseq2d 3998	. . . 4 ⊢ (𝑏 = 𝑑 → ((𝐹‘𝑐) ⊆ (𝐹‘𝑏) ↔ (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
8	5, 7	imbi12d 347	. . 3 ⊢ (𝑏 = 𝑑 → ((𝑐 ⊆ 𝑏 → (𝐹‘𝑐) ⊆ (𝐹‘𝑏)) ↔ (𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑))))
9	4, 8	cbvral2vw 3461	. 2 ⊢ (∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴(𝑎 ⊆ 𝑏 → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) ↔ ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
10		ssun1 4147	. . . . . 6 ⊢ 𝑎 ⊆ (𝑎 ∪ 𝑏)
11		simprl 769	. . . . . . 7 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → 𝑎 ∈ 𝒫 𝐴)
12		pwuncl 7491	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) → (𝑎 ∪ 𝑏) ∈ 𝒫 𝐴)
13	12	adantl 484	. . . . . . 7 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝑎 ∪ 𝑏) ∈ 𝒫 𝐴)
14		simpl 485	. . . . . . 7 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
15		sseq1 3991	. . . . . . . . 9 ⊢ (𝑐 = 𝑎 → (𝑐 ⊆ 𝑑 ↔ 𝑎 ⊆ 𝑑))
16		fveq2 6669	. . . . . . . . . 10 ⊢ (𝑐 = 𝑎 → (𝐹‘𝑐) = (𝐹‘𝑎))
17	16	sseq1d 3997	. . . . . . . . 9 ⊢ (𝑐 = 𝑎 → ((𝐹‘𝑐) ⊆ (𝐹‘𝑑) ↔ (𝐹‘𝑎) ⊆ (𝐹‘𝑑)))
18	15, 17	imbi12d 347	. . . . . . . 8 ⊢ (𝑐 = 𝑎 → ((𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ↔ (𝑎 ⊆ 𝑑 → (𝐹‘𝑎) ⊆ (𝐹‘𝑑))))
19		sseq2 3992	. . . . . . . . 9 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → (𝑎 ⊆ 𝑑 ↔ 𝑎 ⊆ (𝑎 ∪ 𝑏)))
20		fveq2 6669	. . . . . . . . . 10 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → (𝐹‘𝑑) = (𝐹‘(𝑎 ∪ 𝑏)))
21	20	sseq2d 3998	. . . . . . . . 9 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → ((𝐹‘𝑎) ⊆ (𝐹‘𝑑) ↔ (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
22	19, 21	imbi12d 347	. . . . . . . 8 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → ((𝑎 ⊆ 𝑑 → (𝐹‘𝑎) ⊆ (𝐹‘𝑑)) ↔ (𝑎 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))))
23	18, 22	rspc2va 3633	. . . . . . 7 ⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ (𝑎 ∪ 𝑏) ∈ 𝒫 𝐴) ∧ ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑))) → (𝑎 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
24	11, 13, 14, 23	syl21anc 835	. . . . . 6 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝑎 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
25	10, 24	mpi 20	. . . . 5 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
26		ssun2 4148	. . . . . 6 ⊢ 𝑏 ⊆ (𝑎 ∪ 𝑏)
27		simprr 771	. . . . . . 7 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → 𝑏 ∈ 𝒫 𝐴)
28		sseq1 3991	. . . . . . . . 9 ⊢ (𝑐 = 𝑏 → (𝑐 ⊆ 𝑑 ↔ 𝑏 ⊆ 𝑑))
29		fveq2 6669	. . . . . . . . . 10 ⊢ (𝑐 = 𝑏 → (𝐹‘𝑐) = (𝐹‘𝑏))
30	29	sseq1d 3997	. . . . . . . . 9 ⊢ (𝑐 = 𝑏 → ((𝐹‘𝑐) ⊆ (𝐹‘𝑑) ↔ (𝐹‘𝑏) ⊆ (𝐹‘𝑑)))
31	28, 30	imbi12d 347	. . . . . . . 8 ⊢ (𝑐 = 𝑏 → ((𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ↔ (𝑏 ⊆ 𝑑 → (𝐹‘𝑏) ⊆ (𝐹‘𝑑))))
32		sseq2 3992	. . . . . . . . 9 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → (𝑏 ⊆ 𝑑 ↔ 𝑏 ⊆ (𝑎 ∪ 𝑏)))
33	20	sseq2d 3998	. . . . . . . . 9 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → ((𝐹‘𝑏) ⊆ (𝐹‘𝑑) ↔ (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
34	32, 33	imbi12d 347	. . . . . . . 8 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → ((𝑏 ⊆ 𝑑 → (𝐹‘𝑏) ⊆ (𝐹‘𝑑)) ↔ (𝑏 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))))
35	31, 34	rspc2va 3633	. . . . . . 7 ⊢ (((𝑏 ∈ 𝒫 𝐴 ∧ (𝑎 ∪ 𝑏) ∈ 𝒫 𝐴) ∧ ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑))) → (𝑏 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
36	27, 13, 14, 35	syl21anc 835	. . . . . 6 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝑏 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
37	26, 36	mpi 20	. . . . 5 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
38	25, 37	unssd 4161	. . . 4 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
39	38	ralrimivva 3191	. . 3 ⊢ (∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) → ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
40		ssequn1 4155	. . . . 5 ⊢ (𝑐 ⊆ 𝑑 ↔ (𝑐 ∪ 𝑑) = 𝑑)
41	2	uneq1d 4137	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) = ((𝐹‘𝑐) ∪ (𝐹‘𝑏)))
42		uneq1 4131	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝑎 ∪ 𝑏) = (𝑐 ∪ 𝑏))
43	42	fveq2d 6673	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (𝐹‘(𝑎 ∪ 𝑏)) = (𝐹‘(𝑐 ∪ 𝑏)))
44	41, 43	sseq12d 3999	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑐 → (((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ↔ ((𝐹‘𝑐) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑐 ∪ 𝑏))))
45	6	uneq2d 4138	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → ((𝐹‘𝑐) ∪ (𝐹‘𝑏)) = ((𝐹‘𝑐) ∪ (𝐹‘𝑑)))
46		uneq2 4132	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑑 → (𝑐 ∪ 𝑏) = (𝑐 ∪ 𝑑))
47	46	fveq2d 6673	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (𝐹‘(𝑐 ∪ 𝑏)) = (𝐹‘(𝑐 ∪ 𝑑)))
48	45, 47	sseq12d 3999	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑑 → (((𝐹‘𝑐) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑐 ∪ 𝑏)) ↔ ((𝐹‘𝑐) ∪ (𝐹‘𝑑)) ⊆ (𝐹‘(𝑐 ∪ 𝑑))))
49	44, 48	rspc2va 3633	. . . . . . . . . 10 ⊢ (((𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴) ∧ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏))) → ((𝐹‘𝑐) ∪ (𝐹‘𝑑)) ⊆ (𝐹‘(𝑐 ∪ 𝑑)))
50	49	ancoms 461	. . . . . . . . 9 ⊢ ((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) → ((𝐹‘𝑐) ∪ (𝐹‘𝑑)) ⊆ (𝐹‘(𝑐 ∪ 𝑑)))
51	50	unssad 4162	. . . . . . . 8 ⊢ ((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) → (𝐹‘𝑐) ⊆ (𝐹‘(𝑐 ∪ 𝑑)))
52	51	adantr 483	. . . . . . 7 ⊢ (((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐 ∪ 𝑑) = 𝑑) → (𝐹‘𝑐) ⊆ (𝐹‘(𝑐 ∪ 𝑑)))
53		fveq2 6669	. . . . . . . 8 ⊢ ((𝑐 ∪ 𝑑) = 𝑑 → (𝐹‘(𝑐 ∪ 𝑑)) = (𝐹‘𝑑))
54	53	adantl 484	. . . . . . 7 ⊢ (((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐 ∪ 𝑑) = 𝑑) → (𝐹‘(𝑐 ∪ 𝑑)) = (𝐹‘𝑑))
55	52, 54	sseqtrd 4006	. . . . . 6 ⊢ (((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐 ∪ 𝑑) = 𝑑) → (𝐹‘𝑐) ⊆ (𝐹‘𝑑))
56	55	ex 415	. . . . 5 ⊢ ((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) → ((𝑐 ∪ 𝑑) = 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
57	40, 56	syl5bi 244	. . . 4 ⊢ ((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) → (𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
58	57	ralrimivva 3191	. . 3 ⊢ (∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) → ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
59	39, 58	impbii 211	. 2 ⊢ (∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ↔ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
60	9, 59	bitri 277	1 ⊢ (∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴(𝑎 ⊆ 𝑏 → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) ↔ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110  ∀wral 3138   ∪ cun 3933   ⊆ wss 3935  𝒫 cpw 4538  ‘cfv 6354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pr 5329  ax-un 7460

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-br 5066  df-iota 6313  df-fv 6362

This theorem is referenced by: (None)