Theorem isf34lem4 10294

Description: Lemma for isfin3-4 10299. (Contributed by Stefan O'Rear, 7-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)

Hypothesis

Ref	Expression
compss.a	⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥))

Assertion

Ref	Expression
isf34lem4	⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐹‘∪ 𝑋) = ∩ (𝐹 “ 𝑋))

Distinct variable groups:   𝑥,𝐴   𝑥,𝑉

Allowed substitution hints:   𝐹(𝑥)   𝑋(𝑥)

Proof of Theorem isf34lem4

Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sspwuni 5032	. . . . 5 ⊢ (𝑋 ⊆ 𝒫 𝐴 ↔ ∪ 𝑋 ⊆ 𝐴)
2		compss.a	. . . . . 6 ⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥))
3	2	isf34lem1 10289	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ ∪ 𝑋 ⊆ 𝐴) → (𝐹‘∪ 𝑋) = (𝐴 ∖ ∪ 𝑋))
4	1, 3	sylan2b 601	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) → (𝐹‘∪ 𝑋) = (𝐴 ∖ ∪ 𝑋))
5	4	adantrr 724	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐹‘∪ 𝑋) = (𝐴 ∖ ∪ 𝑋))
6		simplrr 784	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑎) ∈ 𝑋)) → ¬ 𝑏 ∈ ∪ 𝑋)
7		simprl 777	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) → 𝑏 ∈ 𝐴)
8	7	ad2antrr 733	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑎) ∈ 𝑋)) ∧ ¬ 𝑏 ∈ 𝑎) → 𝑏 ∈ 𝐴)
9		simpr 486	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑎) ∈ 𝑋)) ∧ ¬ 𝑏 ∈ 𝑎) → ¬ 𝑏 ∈ 𝑎)
10	8, 9	eldifd 3896	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑎) ∈ 𝑋)) ∧ ¬ 𝑏 ∈ 𝑎) → 𝑏 ∈ (𝐴 ∖ 𝑎))
11		simplrr 784	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑎) ∈ 𝑋)) ∧ ¬ 𝑏 ∈ 𝑎) → (𝐴 ∖ 𝑎) ∈ 𝑋)
12		elunii 4846	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ (𝐴 ∖ 𝑎) ∧ (𝐴 ∖ 𝑎) ∈ 𝑋) → 𝑏 ∈ ∪ 𝑋)
13	10, 11, 12	syl2anc 591	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑎) ∈ 𝑋)) ∧ ¬ 𝑏 ∈ 𝑎) → 𝑏 ∈ ∪ 𝑋)
14	13	ex 414	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑎) ∈ 𝑋)) → (¬ 𝑏 ∈ 𝑎 → 𝑏 ∈ ∪ 𝑋))
15	6, 14	mt3d 148	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑎) ∈ 𝑋)) → 𝑏 ∈ 𝑎)
16	15	expr 458	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) ∧ 𝑎 ∈ 𝒫 𝐴) → ((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎))
17	16	ralrimiva 3133	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) → ∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎))
18	17	ex 414	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → ((𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋) → ∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎)))
19		n0 4284	. . . . . . . . 9 ⊢ (𝑋 ≠ ∅ ↔ ∃𝑐 𝑐 ∈ 𝑋)
20		simpr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) → 𝑋 ⊆ 𝒫 𝐴)
21	20	sselda 3917	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) ∧ 𝑐 ∈ 𝑋) → 𝑐 ∈ 𝒫 𝐴)
22	21	elpwid 4541	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) ∧ 𝑐 ∈ 𝑋) → 𝑐 ⊆ 𝐴)
23		dfss4 4200	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ 𝑐)) = 𝑐)
24	22, 23	sylib 220	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) ∧ 𝑐 ∈ 𝑋) → (𝐴 ∖ (𝐴 ∖ 𝑐)) = 𝑐)
25		simpr 486	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) ∧ 𝑐 ∈ 𝑋) → 𝑐 ∈ 𝑋)
26	24, 25	eqeltrd 2841	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) ∧ 𝑐 ∈ 𝑋) → (𝐴 ∖ (𝐴 ∖ 𝑐)) ∈ 𝑋)
27		difss 4069	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∖ 𝑐) ⊆ 𝐴
28		elpw2g 5264	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ 𝑉 → ((𝐴 ∖ 𝑐) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ 𝑐) ⊆ 𝐴))
29	27, 28	mpbiri 260	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝑐) ∈ 𝒫 𝐴)
30	29	ad2antrr 733	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) ∧ 𝑐 ∈ 𝑋) → (𝐴 ∖ 𝑐) ∈ 𝒫 𝐴)
31		difeq2 4054	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝐴 ∖ 𝑐) → (𝐴 ∖ 𝑎) = (𝐴 ∖ (𝐴 ∖ 𝑐)))
32	31	eleq1d 2826	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝐴 ∖ 𝑐) → ((𝐴 ∖ 𝑎) ∈ 𝑋 ↔ (𝐴 ∖ (𝐴 ∖ 𝑐)) ∈ 𝑋))
33		eleq2 2830	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝐴 ∖ 𝑐) → (𝑏 ∈ 𝑎 ↔ 𝑏 ∈ (𝐴 ∖ 𝑐)))
34	32, 33	imbi12d 346	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝐴 ∖ 𝑐) → (((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) ↔ ((𝐴 ∖ (𝐴 ∖ 𝑐)) ∈ 𝑋 → 𝑏 ∈ (𝐴 ∖ 𝑐))))
35	34	rspcv 3558	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∖ 𝑐) ∈ 𝒫 𝐴 → (∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) → ((𝐴 ∖ (𝐴 ∖ 𝑐)) ∈ 𝑋 → 𝑏 ∈ (𝐴 ∖ 𝑐))))
36	30, 35	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) ∧ 𝑐 ∈ 𝑋) → (∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) → ((𝐴 ∖ (𝐴 ∖ 𝑐)) ∈ 𝑋 → 𝑏 ∈ (𝐴 ∖ 𝑐))))
37	26, 36	mpid 44	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) ∧ 𝑐 ∈ 𝑋) → (∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) → 𝑏 ∈ (𝐴 ∖ 𝑐)))
38		eldifi 4064	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ (𝐴 ∖ 𝑐) → 𝑏 ∈ 𝐴)
39	37, 38	syl6 35	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) ∧ 𝑐 ∈ 𝑋) → (∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) → 𝑏 ∈ 𝐴))
40	39	ex 414	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) → (𝑐 ∈ 𝑋 → (∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) → 𝑏 ∈ 𝐴)))
41	40	exlimdv 1941	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) → (∃𝑐 𝑐 ∈ 𝑋 → (∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) → 𝑏 ∈ 𝐴)))
42	19, 41	biimtrid 244	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) → (𝑋 ≠ ∅ → (∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) → 𝑏 ∈ 𝐴)))
43	42	impr 456	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) → 𝑏 ∈ 𝐴))
44		eluni 4844	. . . . . . . . 9 ⊢ (𝑏 ∈ ∪ 𝑋 ↔ ∃𝑐(𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋))
45	29	ad2antrr 733	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋)) → (𝐴 ∖ 𝑐) ∈ 𝒫 𝐴)
46	26	adantlrr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ 𝑐 ∈ 𝑋) → (𝐴 ∖ (𝐴 ∖ 𝑐)) ∈ 𝑋)
47	46	adantrl 723	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋)) → (𝐴 ∖ (𝐴 ∖ 𝑐)) ∈ 𝑋)
48		elndif 4066	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ 𝑐 → ¬ 𝑏 ∈ (𝐴 ∖ 𝑐))
49	48	ad2antrl 735	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋)) → ¬ 𝑏 ∈ (𝐴 ∖ 𝑐))
50	47, 49	jcnd 163	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋)) → ¬ ((𝐴 ∖ (𝐴 ∖ 𝑐)) ∈ 𝑋 → 𝑏 ∈ (𝐴 ∖ 𝑐)))
51	34	notbid 320	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝐴 ∖ 𝑐) → (¬ ((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) ↔ ¬ ((𝐴 ∖ (𝐴 ∖ 𝑐)) ∈ 𝑋 → 𝑏 ∈ (𝐴 ∖ 𝑐))))
52	51	rspcev 3562	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∖ 𝑐) ∈ 𝒫 𝐴 ∧ ¬ ((𝐴 ∖ (𝐴 ∖ 𝑐)) ∈ 𝑋 → 𝑏 ∈ (𝐴 ∖ 𝑐))) → ∃𝑎 ∈ 𝒫 𝐴 ¬ ((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎))
53	45, 50, 52	syl2anc 591	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋)) → ∃𝑎 ∈ 𝒫 𝐴 ¬ ((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎))
54		rexnal 3093	. . . . . . . . . . . 12 ⊢ (∃𝑎 ∈ 𝒫 𝐴 ¬ ((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) ↔ ¬ ∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎))
55	53, 54	sylib 220	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋)) → ¬ ∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎))
56	55	ex 414	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → ((𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋) → ¬ ∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎)))
57	56	exlimdv 1941	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (∃𝑐(𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋) → ¬ ∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎)))
58	44, 57	biimtrid 244	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝑏 ∈ ∪ 𝑋 → ¬ ∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎)))
59	58	con2d 134	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) → ¬ 𝑏 ∈ ∪ 𝑋))
60	43, 59	jcad 518	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) → (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)))
61	18, 60	impbid 214	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → ((𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋) ↔ ∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎)))
62		eldif 3895	. . . . 5 ⊢ (𝑏 ∈ (𝐴 ∖ ∪ 𝑋) ↔ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋))
63		vex 3437	. . . . . 6 ⊢ 𝑏 ∈ V
64	63	elintrab 4893	. . . . 5 ⊢ (𝑏 ∈ ∩ {𝑎 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑎) ∈ 𝑋} ↔ ∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎))
65	61, 62, 64	3bitr4g 316	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝑏 ∈ (𝐴 ∖ ∪ 𝑋) ↔ 𝑏 ∈ ∩ {𝑎 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑎) ∈ 𝑋}))
66	65	eqrdv 2739	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐴 ∖ ∪ 𝑋) = ∩ {𝑎 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑎) ∈ 𝑋})
67	5, 66	eqtrd 2776	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐹‘∪ 𝑋) = ∩ {𝑎 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑎) ∈ 𝑋})
68	2	compss 10293	. . 3 ⊢ (𝐹 “ 𝑋) = {𝑎 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑎) ∈ 𝑋}
69	68	inteqi 4884	. 2 ⊢ ∩ (𝐹 “ 𝑋) = ∩ {𝑎 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑎) ∈ 𝑋}
70	67, 69	eqtr4di 2794	1 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐹‘∪ 𝑋) = ∩ (𝐹 “ 𝑋))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   = wceq 1548  ∃wex 1787   ∈ wcel 2121   ≠ wne 2936  ∀wral 3055  ∃wrex 3065  {crab 3393   ∖ cdif 3882   ⊆ wss 3885  ∅c0 4264  𝒫 cpw 4532  ∪ cuni 4841  ∩ cint 4880   ↦ cmpt 5156   “ cima 5624  ‘cfv 6489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-int 4881  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fv 6497

This theorem is referenced by:  isf34lem5  10295  isf34lem6  10297