Theorem isf34lem5

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

	Ref	Expression
Hypothesis	compss.a	⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) )
Assertion	isf34lem5	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐹 ‘ ∩ 𝑋 ) = ∪ ( 𝐹 “ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		compss.a	⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) )
2		imassrn	⊢ ( 𝐹 “ 𝑋 ) ⊆ ran 𝐹
3	1	isf34lem2	⊢ ( 𝐴 ∈ 𝑉 → 𝐹 : 𝒫 𝐴 ⟶ 𝒫 𝐴 )
4	3	adantr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → 𝐹 : 𝒫 𝐴 ⟶ 𝒫 𝐴 )
5	4	frnd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ran 𝐹 ⊆ 𝒫 𝐴 )
6	2 5	sstrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐹 “ 𝑋 ) ⊆ 𝒫 𝐴 )
7		simprl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → 𝑋 ⊆ 𝒫 𝐴 )
8	4	fdmd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → dom 𝐹 = 𝒫 𝐴 )
9	7 8	sseqtrrd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → 𝑋 ⊆ dom 𝐹 )
10		sseqin2	⊢ ( 𝑋 ⊆ dom 𝐹 ↔ ( dom 𝐹 ∩ 𝑋 ) = 𝑋 )
11	9 10	sylib	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( dom 𝐹 ∩ 𝑋 ) = 𝑋 )
12		simprr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → 𝑋 ≠ ∅ )
13	11 12	eqnetrd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( dom 𝐹 ∩ 𝑋 ) ≠ ∅ )
14		imadisj	⊢ ( ( 𝐹 “ 𝑋 ) = ∅ ↔ ( dom 𝐹 ∩ 𝑋 ) = ∅ )
15	14	necon3bii	⊢ ( ( 𝐹 “ 𝑋 ) ≠ ∅ ↔ ( dom 𝐹 ∩ 𝑋 ) ≠ ∅ )
16	13 15	sylibr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐹 “ 𝑋 ) ≠ ∅ )
17	6 16	jca	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( ( 𝐹 “ 𝑋 ) ⊆ 𝒫 𝐴 ∧ ( 𝐹 “ 𝑋 ) ≠ ∅ ) )
18	1	isf34lem4	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ( 𝐹 “ 𝑋 ) ⊆ 𝒫 𝐴 ∧ ( 𝐹 “ 𝑋 ) ≠ ∅ ) ) → ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑋 ) ) = ∩ ( 𝐹 “ ( 𝐹 “ 𝑋 ) ) )
19	17 18	syldan	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑋 ) ) = ∩ ( 𝐹 “ ( 𝐹 “ 𝑋 ) ) )
20	1	isf34lem3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴 ) → ( 𝐹 “ ( 𝐹 “ 𝑋 ) ) = 𝑋 )
21	20	adantrr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐹 “ ( 𝐹 “ 𝑋 ) ) = 𝑋 )
22	21	inteqd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ∩ ( 𝐹 “ ( 𝐹 “ 𝑋 ) ) = ∩ 𝑋 )
23	19 22	eqtrd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑋 ) ) = ∩ 𝑋 )
24	23	fveq2d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐹 ‘ ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑋 ) ) ) = ( 𝐹 ‘ ∩ 𝑋 ) )
25	1	compsscnv	⊢ ◡ 𝐹 = 𝐹
26	25	fveq1i	⊢ ( ◡ 𝐹 ‘ ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑋 ) ) ) = ( 𝐹 ‘ ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑋 ) ) )
27	1	compssiso	⊢ ( 𝐴 ∈ 𝑉 → 𝐹 Isom [⊊] , ◡ [⊊] ( 𝒫 𝐴 , 𝒫 𝐴 ) )
28		isof1o	⊢ ( 𝐹 Isom [⊊] , ◡ [⊊] ( 𝒫 𝐴 , 𝒫 𝐴 ) → 𝐹 : 𝒫 𝐴 –1-1-onto→ 𝒫 𝐴 )
29	27 28	syl	⊢ ( 𝐴 ∈ 𝑉 → 𝐹 : 𝒫 𝐴 –1-1-onto→ 𝒫 𝐴 )
30		sspwuni	⊢ ( ( 𝐹 “ 𝑋 ) ⊆ 𝒫 𝐴 ↔ ∪ ( 𝐹 “ 𝑋 ) ⊆ 𝐴 )
31	6 30	sylib	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ∪ ( 𝐹 “ 𝑋 ) ⊆ 𝐴 )
32		elpw2g	⊢ ( 𝐴 ∈ 𝑉 → ( ∪ ( 𝐹 “ 𝑋 ) ∈ 𝒫 𝐴 ↔ ∪ ( 𝐹 “ 𝑋 ) ⊆ 𝐴 ) )
33	32	adantr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( ∪ ( 𝐹 “ 𝑋 ) ∈ 𝒫 𝐴 ↔ ∪ ( 𝐹 “ 𝑋 ) ⊆ 𝐴 ) )
34	31 33	mpbird	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ∪ ( 𝐹 “ 𝑋 ) ∈ 𝒫 𝐴 )
35		f1ocnvfv1	⊢ ( ( 𝐹 : 𝒫 𝐴 –1-1-onto→ 𝒫 𝐴 ∧ ∪ ( 𝐹 “ 𝑋 ) ∈ 𝒫 𝐴 ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑋 ) ) ) = ∪ ( 𝐹 “ 𝑋 ) )
36	29 34 35	syl2an2r	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑋 ) ) ) = ∪ ( 𝐹 “ 𝑋 ) )
37	26 36	eqtr3id	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐹 ‘ ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑋 ) ) ) = ∪ ( 𝐹 “ 𝑋 ) )
38	24 37	eqtr3d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐹 ‘ ∩ 𝑋 ) = ∪ ( 𝐹 “ 𝑋 ) )