Theorem qtopcmplem

Description: Lemma for qtopcmp and qtopconn . (Contributed by Mario Carneiro, 24-Mar-2015)

	Ref	Expression
Hypotheses	qtopcmp.1	⊢ 𝑋 = ∪ 𝐽
	qtopcmplem.1	⊢ ( 𝐽 ∈ 𝐴 → 𝐽 ∈ Top )
	qtopcmplem.2	⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝐹 : 𝑋 –onto→ ∪ ( 𝐽 qTop 𝐹 ) ∧ 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) ) → ( 𝐽 qTop 𝐹 ) ∈ 𝐴 )
Assertion	qtopcmplem	⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝐹 Fn 𝑋 ) → ( 𝐽 qTop 𝐹 ) ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		qtopcmp.1	⊢ 𝑋 = ∪ 𝐽
2		qtopcmplem.1	⊢ ( 𝐽 ∈ 𝐴 → 𝐽 ∈ Top )
3		qtopcmplem.2	⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝐹 : 𝑋 –onto→ ∪ ( 𝐽 qTop 𝐹 ) ∧ 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) ) → ( 𝐽 qTop 𝐹 ) ∈ 𝐴 )
4		simpl	⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝐹 Fn 𝑋 ) → 𝐽 ∈ 𝐴 )
5		simpr	⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝐹 Fn 𝑋 ) → 𝐹 Fn 𝑋 )
6		dffn4	⊢ ( 𝐹 Fn 𝑋 ↔ 𝐹 : 𝑋 –onto→ ran 𝐹 )
7	5 6	sylib	⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝐹 Fn 𝑋 ) → 𝐹 : 𝑋 –onto→ ran 𝐹 )
8	1	qtopuni	⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 : 𝑋 –onto→ ran 𝐹 ) → ran 𝐹 = ∪ ( 𝐽 qTop 𝐹 ) )
9	2 8	sylan	⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝐹 : 𝑋 –onto→ ran 𝐹 ) → ran 𝐹 = ∪ ( 𝐽 qTop 𝐹 ) )
10	6 9	sylan2b	⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝐹 Fn 𝑋 ) → ran 𝐹 = ∪ ( 𝐽 qTop 𝐹 ) )
11		foeq3	⊢ ( ran 𝐹 = ∪ ( 𝐽 qTop 𝐹 ) → ( 𝐹 : 𝑋 –onto→ ran 𝐹 ↔ 𝐹 : 𝑋 –onto→ ∪ ( 𝐽 qTop 𝐹 ) ) )
12	10 11	syl	⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝐹 Fn 𝑋 ) → ( 𝐹 : 𝑋 –onto→ ran 𝐹 ↔ 𝐹 : 𝑋 –onto→ ∪ ( 𝐽 qTop 𝐹 ) ) )
13	7 12	mpbid	⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝐹 Fn 𝑋 ) → 𝐹 : 𝑋 –onto→ ∪ ( 𝐽 qTop 𝐹 ) )
14	1	toptopon	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
15	2 14	sylib	⊢ ( 𝐽 ∈ 𝐴 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
16		qtopid	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) )
17	15 16	sylan	⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝐹 Fn 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) )
18	4 13 17 3	syl3anc	⊢ ( ( 𝐽 ∈ 𝐴 ∧ 𝐹 Fn 𝑋 ) → ( 𝐽 qTop 𝐹 ) ∈ 𝐴 )