Theorem ssunsn2 3866

Description: The property of being sandwiched between two sets naturally splits under union with a singleton. This is the induction hypothesis for the determination of large powersets such as pwtp 3885. (Contributed by Mario Carneiro, 2-Jul-2016.)

Assertion

Ref	Expression
ssunsn2	⊢ ((B ⊆ A ∧ A ⊆ (C ∪ {D})) ↔ ((B ⊆ A ∧ A ⊆ C) ∨ ((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {D}))))

Proof of Theorem ssunsn2

Step	Hyp	Ref	Expression
1		snssi 3853	. . . . 5 ⊢ (D ∈ A → {D} ⊆ A)
2		unss 3438	. . . . . . 7 ⊢ ((B ⊆ A ∧ {D} ⊆ A) ↔ (B ∪ {D}) ⊆ A)
3	2	bicomi 193	. . . . . 6 ⊢ ((B ∪ {D}) ⊆ A ↔ (B ⊆ A ∧ {D} ⊆ A))
4	3	rbaibr 874	. . . . 5 ⊢ ({D} ⊆ A → (B ⊆ A ↔ (B ∪ {D}) ⊆ A))
5	1, 4	syl 15	. . . 4 ⊢ (D ∈ A → (B ⊆ A ↔ (B ∪ {D}) ⊆ A))
6	5	anbi1d 685	. . 3 ⊢ (D ∈ A → ((B ⊆ A ∧ A ⊆ (C ∪ {D})) ↔ ((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {D}))))
7	2	biimpi 186	. . . . . . 7 ⊢ ((B ⊆ A ∧ {D} ⊆ A) → (B ∪ {D}) ⊆ A)
8	7	expcom 424	. . . . . 6 ⊢ ({D} ⊆ A → (B ⊆ A → (B ∪ {D}) ⊆ A))
9	1, 8	syl 15	. . . . 5 ⊢ (D ∈ A → (B ⊆ A → (B ∪ {D}) ⊆ A))
10		ssun3 3429	. . . . . 6 ⊢ (A ⊆ C → A ⊆ (C ∪ {D}))
11	10	a1i 10	. . . . 5 ⊢ (D ∈ A → (A ⊆ C → A ⊆ (C ∪ {D})))
12	9, 11	anim12d 546	. . . 4 ⊢ (D ∈ A → ((B ⊆ A ∧ A ⊆ C) → ((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {D}))))
13		pm4.72 846	. . . 4 ⊢ (((B ⊆ A ∧ A ⊆ C) → ((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {D}))) ↔ (((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {D})) ↔ ((B ⊆ A ∧ A ⊆ C) ∨ ((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {D})))))
14	12, 13	sylib 188	. . 3 ⊢ (D ∈ A → (((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {D})) ↔ ((B ⊆ A ∧ A ⊆ C) ∨ ((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {D})))))
15	6, 14	bitrd 244	. 2 ⊢ (D ∈ A → ((B ⊆ A ∧ A ⊆ (C ∪ {D})) ↔ ((B ⊆ A ∧ A ⊆ C) ∨ ((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {D})))))
16		disjsn 3787	. . . . . . 7 ⊢ ((A ∩ {D}) = ∅ ↔ ¬ D ∈ A)
17		disj3 3596	. . . . . . 7 ⊢ ((A ∩ {D}) = ∅ ↔ A = (A ∖ {D}))
18	16, 17	bitr3i 242	. . . . . 6 ⊢ (¬ D ∈ A ↔ A = (A ∖ {D}))
19		sseq1 3293	. . . . . 6 ⊢ (A = (A ∖ {D}) → (A ⊆ C ↔ (A ∖ {D}) ⊆ C))
20	18, 19	sylbi 187	. . . . 5 ⊢ (¬ D ∈ A → (A ⊆ C ↔ (A ∖ {D}) ⊆ C))
21		uncom 3409	. . . . . . 7 ⊢ ({D} ∪ C) = (C ∪ {D})
22	21	sseq2i 3297	. . . . . 6 ⊢ (A ⊆ ({D} ∪ C) ↔ A ⊆ (C ∪ {D}))
23		ssundif 3634	. . . . . 6 ⊢ (A ⊆ ({D} ∪ C) ↔ (A ∖ {D}) ⊆ C)
24	22, 23	bitr3i 242	. . . . 5 ⊢ (A ⊆ (C ∪ {D}) ↔ (A ∖ {D}) ⊆ C)
25	20, 24	syl6rbbr 255	. . . 4 ⊢ (¬ D ∈ A → (A ⊆ (C ∪ {D}) ↔ A ⊆ C))
26	25	anbi2d 684	. . 3 ⊢ (¬ D ∈ A → ((B ⊆ A ∧ A ⊆ (C ∪ {D})) ↔ (B ⊆ A ∧ A ⊆ C)))
27	3	simplbi 446	. . . . . . 7 ⊢ ((B ∪ {D}) ⊆ A → B ⊆ A)
28	27	a1i 10	. . . . . 6 ⊢ (¬ D ∈ A → ((B ∪ {D}) ⊆ A → B ⊆ A))
29	25	biimpd 198	. . . . . 6 ⊢ (¬ D ∈ A → (A ⊆ (C ∪ {D}) → A ⊆ C))
30	28, 29	anim12d 546	. . . . 5 ⊢ (¬ D ∈ A → (((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {D})) → (B ⊆ A ∧ A ⊆ C)))
31		pm4.72 846	. . . . 5 ⊢ ((((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {D})) → (B ⊆ A ∧ A ⊆ C)) ↔ ((B ⊆ A ∧ A ⊆ C) ↔ (((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {D})) ∨ (B ⊆ A ∧ A ⊆ C))))
32	30, 31	sylib 188	. . . 4 ⊢ (¬ D ∈ A → ((B ⊆ A ∧ A ⊆ C) ↔ (((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {D})) ∨ (B ⊆ A ∧ A ⊆ C))))
33		orcom 376	. . . 4 ⊢ ((((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {D})) ∨ (B ⊆ A ∧ A ⊆ C)) ↔ ((B ⊆ A ∧ A ⊆ C) ∨ ((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {D}))))
34	32, 33	syl6bb 252	. . 3 ⊢ (¬ D ∈ A → ((B ⊆ A ∧ A ⊆ C) ↔ ((B ⊆ A ∧ A ⊆ C) ∨ ((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {D})))))
35	26, 34	bitrd 244	. 2 ⊢ (¬ D ∈ A → ((B ⊆ A ∧ A ⊆ (C ∪ {D})) ↔ ((B ⊆ A ∧ A ⊆ C) ∨ ((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {D})))))
36	15, 35	pm2.61i 156	1 ⊢ ((B ⊆ A ∧ A ⊆ (C ∪ {D})) ↔ ((B ⊆ A ∧ A ⊆ C) ∨ ((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {D}))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∨ wo 357   ∧ wa 358   = wceq 1642   ∈ wcel 1710   ∖ cdif 3207   ∪ cun 3208   ∩ cin 3209   ⊆ wss 3258  ∅c0 3551  {csn 3738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-ss 3260  df-nul 3552  df-sn 3742

This theorem is referenced by:  ssunsn  3867  ssunpr  3869  sstp  3871