Theorem isotone1 45033

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 3956	. . . 4 ⊢ (𝑎 = 𝑐 → (𝑎 ⊆ 𝑏 ↔ 𝑐 ⊆ 𝑏))
2		fveq2 6883	. . . . 5 ⊢ (𝑎 = 𝑐 → (𝐹‘𝑎) = (𝐹‘𝑐))
3	2	sseq1d 3962	. . . 4 ⊢ (𝑎 = 𝑐 → ((𝐹‘𝑎) ⊆ (𝐹‘𝑏) ↔ (𝐹‘𝑐) ⊆ (𝐹‘𝑏)))
4	1, 3	imbi12d 347	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 ⊆ 𝑏 → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) ↔ (𝑐 ⊆ 𝑏 → (𝐹‘𝑐) ⊆ (𝐹‘𝑏))))
5		sseq2 3957	. . . 4 ⊢ (𝑏 = 𝑑 → (𝑐 ⊆ 𝑏 ↔ 𝑐 ⊆ 𝑑))
6		fveq2 6883	. . . . 5 ⊢ (𝑏 = 𝑑 → (𝐹‘𝑏) = (𝐹‘𝑑))
7	6	sseq2d 3963	. . . 4 ⊢ (𝑏 = 𝑑 → ((𝐹‘𝑐) ⊆ (𝐹‘𝑏) ↔ (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
8	5, 7	imbi12d 347	. . 3 ⊢ (𝑏 = 𝑑 → ((𝑐 ⊆ 𝑏 → (𝐹‘𝑐) ⊆ (𝐹‘𝑏)) ↔ (𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑))))
9	4, 8	cbvral2vw 3245	. 2 ⊢ (∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴(𝑎 ⊆ 𝑏 → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) ↔ ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
10		ssun1 4124	. . . . . 6 ⊢ 𝑎 ⊆ (𝑎 ∪ 𝑏)
11		simprl 783	. . . . . . 7 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → 𝑎 ∈ 𝒫 𝐴)
12		pwuncl 7782	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) → (𝑎 ∪ 𝑏) ∈ 𝒫 𝐴)
13	12	adantl 487	. . . . . . 7 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝑎 ∪ 𝑏) ∈ 𝒫 𝐴)
14		simpl 488	. . . . . . 7 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
15		sseq1 3956	. . . . . . . . 9 ⊢ (𝑐 = 𝑎 → (𝑐 ⊆ 𝑑 ↔ 𝑎 ⊆ 𝑑))
16		fveq2 6883	. . . . . . . . . 10 ⊢ (𝑐 = 𝑎 → (𝐹‘𝑐) = (𝐹‘𝑎))
17	16	sseq1d 3962	. . . . . . . . 9 ⊢ (𝑐 = 𝑎 → ((𝐹‘𝑐) ⊆ (𝐹‘𝑑) ↔ (𝐹‘𝑎) ⊆ (𝐹‘𝑑)))
18	15, 17	imbi12d 347	. . . . . . . 8 ⊢ (𝑐 = 𝑎 → ((𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ↔ (𝑎 ⊆ 𝑑 → (𝐹‘𝑎) ⊆ (𝐹‘𝑑))))
19		sseq2 3957	. . . . . . . . 9 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → (𝑎 ⊆ 𝑑 ↔ 𝑎 ⊆ (𝑎 ∪ 𝑏)))
20		fveq2 6883	. . . . . . . . . 10 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → (𝐹‘𝑑) = (𝐹‘(𝑎 ∪ 𝑏)))
21	20	sseq2d 3963	. . . . . . . . 9 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → ((𝐹‘𝑎) ⊆ (𝐹‘𝑑) ↔ (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
22	19, 21	imbi12d 347	. . . . . . . 8 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → ((𝑎 ⊆ 𝑑 → (𝐹‘𝑎) ⊆ (𝐹‘𝑑)) ↔ (𝑎 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))))
23	18, 22	rspc2va 3588	. . . . . . 7 ⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ (𝑎 ∪ 𝑏) ∈ 𝒫 𝐴) ∧ ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑))) → (𝑎 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
24	11, 13, 14, 23	syl21anc 851	. . . . . 6 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝑎 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
25	10, 24	mpi 21	. . . . 5 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝐹‘𝑎) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
26		ssun2 4125	. . . . . 6 ⊢ 𝑏 ⊆ (𝑎 ∪ 𝑏)
27		simprr 785	. . . . . . 7 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → 𝑏 ∈ 𝒫 𝐴)
28		sseq1 3956	. . . . . . . . 9 ⊢ (𝑐 = 𝑏 → (𝑐 ⊆ 𝑑 ↔ 𝑏 ⊆ 𝑑))
29		fveq2 6883	. . . . . . . . . 10 ⊢ (𝑐 = 𝑏 → (𝐹‘𝑐) = (𝐹‘𝑏))
30	29	sseq1d 3962	. . . . . . . . 9 ⊢ (𝑐 = 𝑏 → ((𝐹‘𝑐) ⊆ (𝐹‘𝑑) ↔ (𝐹‘𝑏) ⊆ (𝐹‘𝑑)))
31	28, 30	imbi12d 347	. . . . . . . 8 ⊢ (𝑐 = 𝑏 → ((𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ↔ (𝑏 ⊆ 𝑑 → (𝐹‘𝑏) ⊆ (𝐹‘𝑑))))
32		sseq2 3957	. . . . . . . . 9 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → (𝑏 ⊆ 𝑑 ↔ 𝑏 ⊆ (𝑎 ∪ 𝑏)))
33	20	sseq2d 3963	. . . . . . . . 9 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → ((𝐹‘𝑏) ⊆ (𝐹‘𝑑) ↔ (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
34	32, 33	imbi12d 347	. . . . . . . 8 ⊢ (𝑑 = (𝑎 ∪ 𝑏) → ((𝑏 ⊆ 𝑑 → (𝐹‘𝑏) ⊆ (𝐹‘𝑑)) ↔ (𝑏 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))))
35	31, 34	rspc2va 3588	. . . . . . 7 ⊢ (((𝑏 ∈ 𝒫 𝐴 ∧ (𝑎 ∪ 𝑏) ∈ 𝒫 𝐴) ∧ ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑))) → (𝑏 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
36	27, 13, 14, 35	syl21anc 851	. . . . . 6 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝑏 ⊆ (𝑎 ∪ 𝑏) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏))))
37	26, 36	mpi 21	. . . . 5 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
38	25, 37	unssd 4138	. . . 4 ⊢ ((∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴)) → ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
39	38	ralrimivva 3206	. . 3 ⊢ (∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) → ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
40		ssequn1 4132	. . . . 5 ⊢ (𝑐 ⊆ 𝑑 ↔ (𝑐 ∪ 𝑑) = 𝑑)
41	2	uneq1d 4114	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → ((𝐹‘𝑎) ∪ (𝐹‘𝑏)) = ((𝐹‘𝑐) ∪ (𝐹‘𝑏)))
42		uneq1 4108	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝑎 ∪ 𝑏) = (𝑐 ∪ 𝑏))
43	42	fveq2d 6887	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (𝐹‘(𝑎 ∪ 𝑏)) = (𝐹‘(𝑐 ∪ 𝑏)))
44	41, 43	sseq12d 3964	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑐 → (((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ↔ ((𝐹‘𝑐) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑐 ∪ 𝑏))))
45	6	uneq2d 4115	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → ((𝐹‘𝑐) ∪ (𝐹‘𝑏)) = ((𝐹‘𝑐) ∪ (𝐹‘𝑑)))
46		uneq2 4109	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑑 → (𝑐 ∪ 𝑏) = (𝑐 ∪ 𝑑))
47	46	fveq2d 6887	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (𝐹‘(𝑐 ∪ 𝑏)) = (𝐹‘(𝑐 ∪ 𝑑)))
48	45, 47	sseq12d 3964	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑑 → (((𝐹‘𝑐) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑐 ∪ 𝑏)) ↔ ((𝐹‘𝑐) ∪ (𝐹‘𝑑)) ⊆ (𝐹‘(𝑐 ∪ 𝑑))))
49	44, 48	rspc2va 3588	. . . . . . . . . 10 ⊢ (((𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴) ∧ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏))) → ((𝐹‘𝑐) ∪ (𝐹‘𝑑)) ⊆ (𝐹‘(𝑐 ∪ 𝑑)))
50	49	ancoms 464	. . . . . . . . 9 ⊢ ((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) → ((𝐹‘𝑐) ∪ (𝐹‘𝑑)) ⊆ (𝐹‘(𝑐 ∪ 𝑑)))
51	50	unssad 4139	. . . . . . . 8 ⊢ ((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) → (𝐹‘𝑐) ⊆ (𝐹‘(𝑐 ∪ 𝑑)))
52	51	adantr 486	. . . . . . 7 ⊢ (((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐 ∪ 𝑑) = 𝑑) → (𝐹‘𝑐) ⊆ (𝐹‘(𝑐 ∪ 𝑑)))
53		fveq2 6883	. . . . . . . 8 ⊢ ((𝑐 ∪ 𝑑) = 𝑑 → (𝐹‘(𝑐 ∪ 𝑑)) = (𝐹‘𝑑))
54	53	adantl 487	. . . . . . 7 ⊢ (((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐 ∪ 𝑑) = 𝑑) → (𝐹‘(𝑐 ∪ 𝑑)) = (𝐹‘𝑑))
55	52, 54	sseqtrd 3967	. . . . . 6 ⊢ (((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) ∧ (𝑐 ∪ 𝑑) = 𝑑) → (𝐹‘𝑐) ⊆ (𝐹‘𝑑))
56	55	ex 418	. . . . 5 ⊢ ((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) → ((𝑐 ∪ 𝑑) = 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
57	40, 56	biimtrid 245	. . . 4 ⊢ ((∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) ∧ (𝑐 ∈ 𝒫 𝐴 ∧ 𝑑 ∈ 𝒫 𝐴)) → (𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
58	57	ralrimivva 3206	. . 3 ⊢ (∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)) → ∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)))
59	39, 58	impbii 212	. 2 ⊢ (∀𝑐 ∈ 𝒫 𝐴∀𝑑 ∈ 𝒫 𝐴(𝑐 ⊆ 𝑑 → (𝐹‘𝑐) ⊆ (𝐹‘𝑑)) ↔ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))
60	9, 59	bitri 278	1 ⊢ (∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴(𝑎 ⊆ 𝑏 → (𝐹‘𝑎) ⊆ (𝐹‘𝑏)) ↔ ∀𝑎 ∈ 𝒫 𝐴∀𝑏 ∈ 𝒫 𝐴((𝐹‘𝑎) ∪ (𝐹‘𝑏)) ⊆ (𝐹‘(𝑎 ∪ 𝑏)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3077   ∪ cun 3897   ⊆ wss 3899  𝒫 cpw 4557  ‘cfv 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391  ax-un 7749

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545

This theorem is used by: (None)