Theorem fmfnfmlem4 23910

Description: Lemma for fmfnfm 23911. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)

Hypotheses

Ref	Expression
fmfnfm.b	⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌))
fmfnfm.l	⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋))
fmfnfm.f	⊢ (𝜑 → 𝐹:𝑌⟶𝑋)
fmfnfm.fm	⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)

Assertion

Ref	Expression
fmfnfmlem4	⊢ (𝜑 → (𝑡 ∈ 𝐿 ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡)))

Distinct variable groups:   𝑡,𝑠,𝑥,𝐵   𝐹,𝑠,𝑡,𝑥   𝐿,𝑠,𝑡,𝑥   𝜑,𝑠,𝑡,𝑥   𝑋,𝑠,𝑡,𝑥   𝑌,𝑠,𝑡,𝑥

Proof of Theorem fmfnfmlem4

Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fmfnfm.l	. . . 4 ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋))
2		filelss 23805	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑡 ∈ 𝐿) → 𝑡 ⊆ 𝑋)
3	2	ex 412	. . . 4 ⊢ (𝐿 ∈ (Fil‘𝑋) → (𝑡 ∈ 𝐿 → 𝑡 ⊆ 𝑋))
4	1, 3	syl 17	. . 3 ⊢ (𝜑 → (𝑡 ∈ 𝐿 → 𝑡 ⊆ 𝑋))
5		fmfnfm.b	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌))
6		mptexg 7165	. . . . . . . . . . 11 ⊢ (𝐿 ∈ (Fil‘𝑋) → (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V)
7		rnexg 7842	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V)
8	6, 7	syl 17	. . . . . . . . . 10 ⊢ (𝐿 ∈ (Fil‘𝑋) → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V)
9	1, 8	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V)
10		unexg 7686	. . . . . . . . 9 ⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V) → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ V)
11	5, 9, 10	syl2anc 585	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ V)
12		ssfii 9321	. . . . . . . . 9 ⊢ ((𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ V → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))))
13	12	unssbd 4125	. . . . . . . 8 ⊢ ((𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ V → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))))
14	11, 13	syl 17	. . . . . . 7 ⊢ (𝜑 → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))))
15	14	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))))
16		eqid 2735	. . . . . . . . 9 ⊢ (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑡)
17		imaeq2 6010	. . . . . . . . . 10 ⊢ (𝑥 = 𝑡 → (◡𝐹 “ 𝑥) = (◡𝐹 “ 𝑡))
18	17	rspceeqv 3585	. . . . . . . . 9 ⊢ ((𝑡 ∈ 𝐿 ∧ (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑡)) → ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥))
19	16, 18	mpan2 692	. . . . . . . 8 ⊢ (𝑡 ∈ 𝐿 → ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥))
20	19	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥))
21		elfvdm 6863	. . . . . . . . . . 11 ⊢ (𝐵 ∈ (fBas‘𝑌) → 𝑌 ∈ dom fBas)
22	5, 21	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ dom fBas)
23		cnvimass 6036	. . . . . . . . . . 11 ⊢ (◡𝐹 “ 𝑡) ⊆ dom 𝐹
24		fmfnfm.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝑌⟶𝑋)
25	23, 24	fssdm 6676	. . . . . . . . . 10 ⊢ (𝜑 → (◡𝐹 “ 𝑡) ⊆ 𝑌)
26	22, 25	ssexd 5254	. . . . . . . . 9 ⊢ (𝜑 → (◡𝐹 “ 𝑡) ∈ V)
27	26	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → (◡𝐹 “ 𝑡) ∈ V)
28		eqid 2735	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) = (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))
29	28	elrnmpt 5902	. . . . . . . 8 ⊢ ((◡𝐹 “ 𝑡) ∈ V → ((◡𝐹 “ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥)))
30	27, 29	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → ((◡𝐹 “ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (◡𝐹 “ 𝑡) = (◡𝐹 “ 𝑥)))
31	20, 30	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → (◡𝐹 “ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))
32	15, 31	sseldd 3918	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → (◡𝐹 “ 𝑡) ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))))
33		ffun 6660	. . . . . . . 8 ⊢ (𝐹:𝑌⟶𝑋 → Fun 𝐹)
34		ssid 3939	. . . . . . . 8 ⊢ (◡𝐹 “ 𝑡) ⊆ (◡𝐹 “ 𝑡)
35		funimass2 6570	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ (◡𝐹 “ 𝑡) ⊆ (◡𝐹 “ 𝑡)) → (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡)
36	33, 34, 35	sylancl 587	. . . . . . 7 ⊢ (𝐹:𝑌⟶𝑋 → (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡)
37	24, 36	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡)
38	37	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡)
39		imaeq2 6010	. . . . . . 7 ⊢ (𝑠 = (◡𝐹 “ 𝑡) → (𝐹 “ 𝑠) = (𝐹 “ (◡𝐹 “ 𝑡)))
40	39	sseq1d 3948	. . . . . 6 ⊢ (𝑠 = (◡𝐹 “ 𝑡) → ((𝐹 “ 𝑠) ⊆ 𝑡 ↔ (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡))
41	40	rspcev 3562	. . . . 5 ⊢ (((◡𝐹 “ 𝑡) ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ∧ (𝐹 “ (◡𝐹 “ 𝑡)) ⊆ 𝑡) → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡)
42	32, 38, 41	syl2anc 585	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡)
43	42	ex 412	. . 3 ⊢ (𝜑 → (𝑡 ∈ 𝐿 → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡))
44	4, 43	jcad 512	. 2 ⊢ (𝜑 → (𝑡 ∈ 𝐿 → (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡)))
45		elfiun 9332	. . . . . 6 ⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V) → (𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ↔ (𝑠 ∈ (fi‘𝐵) ∨ 𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∨ ∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))𝑠 = (𝑧 ∩ 𝑤))))
46	5, 9, 45	syl2anc 585	. . . . 5 ⊢ (𝜑 → (𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ↔ (𝑠 ∈ (fi‘𝐵) ∨ 𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∨ ∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))𝑠 = (𝑧 ∩ 𝑤))))
47		fmfnfm.fm	. . . . . . 7 ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)
48	5, 1, 24, 47	fmfnfmlem1 23907	. . . . . 6 ⊢ (𝜑 → (𝑠 ∈ (fi‘𝐵) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
49	5, 1, 24, 47	fmfnfmlem3 23909	. . . . . . . 8 ⊢ (𝜑 → (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) = ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))
50	49	eleq2d 2821	. . . . . . 7 ⊢ (𝜑 → (𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ↔ 𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))
51	28	elrnmpt 5902	. . . . . . . . 9 ⊢ (𝑠 ∈ V → (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥)))
52	51	elv 3432	. . . . . . . 8 ⊢ (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥))
53	5, 1, 24, 47	fmfnfmlem2 23908	. . . . . . . 8 ⊢ (𝜑 → (∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
54	52, 53	biimtrid 242	. . . . . . 7 ⊢ (𝜑 → (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
55	50, 54	sylbid 240	. . . . . 6 ⊢ (𝜑 → (𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
56	49	eleq2d 2821	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ↔ 𝑤 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))
57	28	elrnmpt 5902	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ V → (𝑤 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥)))
58	57	elv 3432	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥))
59	56, 58	bitrdi 287	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ↔ ∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥)))
60	59	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (fi‘𝐵)) → (𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ↔ ∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥)))
61		fbssfi 23790	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑧 ∈ (fi‘𝐵)) → ∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧)
62	5, 61	sylan 581	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (fi‘𝐵)) → ∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧)
63	1	ad3antrrr 731	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝐿 ∈ (Fil‘𝑋))
64	1	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → 𝐿 ∈ (Fil‘𝑋))
65	47	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)
66		filtop 23808	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐿 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐿)
67	1, 66	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑋 ∈ 𝐿)
68	67, 5, 24	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋))
69	68	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋))
70		ssfg 23825	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ (𝑌filGen𝐵))
71	5, 70	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐵 ⊆ (𝑌filGen𝐵))
72	71	sselda 3917	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈ (𝑌filGen𝐵))
73		eqid 2735	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑌filGen𝐵) = (𝑌filGen𝐵)
74	73	imaelfm 23904	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑠 ∈ (𝑌filGen𝐵)) → (𝐹 “ 𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
75	69, 72, 74	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝐹 “ 𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
76	65, 75	sseldd 3918	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝐹 “ 𝑠) ∈ 𝐿)
77	76	adantrr 718	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → (𝐹 “ 𝑠) ∈ 𝐿)
78	64, 77	jca 511	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → (𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿))
79		filin 23807	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿 ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿)
80	79	3expa 1119	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿)
81	78, 80	sylan 581	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿)
82	81	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿)
83		simprr 773	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝑡 ⊆ 𝑋)
84		elin 3901	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) ↔ (𝑤 ∈ (𝐹 “ 𝑠) ∧ 𝑤 ∈ 𝑥))
85	24, 33	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → Fun 𝐹)
86		fvelima 6894	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((Fun 𝐹 ∧ 𝑤 ∈ (𝐹 “ 𝑠)) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑤)
87	86	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Fun 𝐹 → (𝑤 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑤))
88	85, 87	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑤 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑤))
89	88	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → (𝑤 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑤))
90	85	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → Fun 𝐹)
91		simplrr 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) → 𝑠 ⊆ 𝑧)
92		simprl 771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥)) → 𝑦 ∈ 𝑠)
93		ssel2 3912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑠 ⊆ 𝑧 ∧ 𝑦 ∈ 𝑠) → 𝑦 ∈ 𝑧)
94	91, 92, 93	syl2an 597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → 𝑦 ∈ 𝑧)
95	85	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝑠) → Fun 𝐹)
96		fbelss 23786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ 𝑌)
97	5, 96	sylan 581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ 𝑌)
98	24	fdmd 6667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → dom 𝐹 = 𝑌)
99	98	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → dom 𝐹 = 𝑌)
100	97, 99	sseqtrrd 3954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ dom 𝐹)
101	100	adantrr 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → 𝑠 ⊆ dom 𝐹)
102	101	sselda 3917	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝑠) → 𝑦 ∈ dom 𝐹)
103		fvimacnv 6994	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹) → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑦 ∈ (◡𝐹 “ 𝑥)))
104	95, 102, 103	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑦 ∈ (◡𝐹 “ 𝑥)))
105	104	biimpd 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 → 𝑦 ∈ (◡𝐹 “ 𝑥)))
106	105	impr 454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥)) → 𝑦 ∈ (◡𝐹 “ 𝑥))
107	106	ad2ant2rl 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → 𝑦 ∈ (◡𝐹 “ 𝑥))
108	94, 107	elind 4131	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → 𝑦 ∈ (𝑧 ∩ (◡𝐹 “ 𝑥)))
109		inss2 4168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 ∩ (◡𝐹 “ 𝑥)) ⊆ (◡𝐹 “ 𝑥)
110		cnvimass 6036	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (◡𝐹 “ 𝑥) ⊆ dom 𝐹
111	109, 110	sstri 3926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 ∩ (◡𝐹 “ 𝑥)) ⊆ dom 𝐹
112		funfvima2 7175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((Fun 𝐹 ∧ (𝑧 ∩ (◡𝐹 “ 𝑥)) ⊆ dom 𝐹) → (𝑦 ∈ (𝑧 ∩ (◡𝐹 “ 𝑥)) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))))
113	111, 112	mpan2 692	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (Fun 𝐹 → (𝑦 ∈ (𝑧 ∩ (◡𝐹 “ 𝑥)) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))))
114	90, 108, 113	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))
115	114	anassrs 467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥)) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))
116	115	expr 456	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))))
117		eleq1 2823	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹‘𝑦) = 𝑤 → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑤 ∈ 𝑥))
118		eleq1 2823	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹‘𝑦) = 𝑤 → ((𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ↔ 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))))
119	117, 118	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹‘𝑦) = 𝑤 → (((𝐹‘𝑦) ∈ 𝑥 → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))) ↔ (𝑤 ∈ 𝑥 → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))))
120	116, 119	syl5ibcom 245	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) = 𝑤 → (𝑤 ∈ 𝑥 → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))))
121	120	rexlimdva 3136	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → (∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑤 → (𝑤 ∈ 𝑥 → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))))
122	89, 121	syld 47	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → (𝑤 ∈ (𝐹 “ 𝑠) → (𝑤 ∈ 𝑥 → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))))
123	122	impd 410	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → ((𝑤 ∈ (𝐹 “ 𝑠) ∧ 𝑤 ∈ 𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))))
124	84, 123	biimtrid 242	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → (𝑤 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))))
125	124	adantrl 717	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝑤 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥)))))
126	125	ssrdv 3923	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ((𝐹 “ 𝑠) ∩ 𝑥) ⊆ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))
127		simprl 771	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡)
128	126, 127	sstrd 3927	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ((𝐹 “ 𝑠) ∩ 𝑥) ⊆ 𝑡)
129		filss 23806	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ (((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿 ∧ 𝑡 ⊆ 𝑋 ∧ ((𝐹 “ 𝑠) ∩ 𝑥) ⊆ 𝑡)) → 𝑡 ∈ 𝐿)
130	63, 82, 83, 128, 129	syl13anc 1375	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝑡 ∈ 𝐿)
131	130	exp32 420	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))
132		ineq2 4145	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = (◡𝐹 “ 𝑥) → (𝑧 ∩ 𝑤) = (𝑧 ∩ (◡𝐹 “ 𝑥)))
133	132	imaeq2d 6014	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = (◡𝐹 “ 𝑥) → (𝐹 “ (𝑧 ∩ 𝑤)) = (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))))
134	133	sseq1d 3948	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 ↔ (𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡))
135	134	imbi1d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (◡𝐹 “ 𝑥) → (((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)) ↔ ((𝐹 “ (𝑧 ∩ (◡𝐹 “ 𝑥))) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
136	131, 135	syl5ibrcom 247	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) → (𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
137	136	rexlimdva 3136	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → (∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
138	137	rexlimdvaa 3137	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧 → (∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))))
139	138	imp 406	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧) → (∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
140	62, 139	syldan 592	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (fi‘𝐵)) → (∃𝑥 ∈ 𝐿 𝑤 = (◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
141	60, 140	sylbid 240	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (fi‘𝐵)) → (𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
142	141	impr 454	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))
143		imaeq2 6010	. . . . . . . . . 10 ⊢ (𝑠 = (𝑧 ∩ 𝑤) → (𝐹 “ 𝑠) = (𝐹 “ (𝑧 ∩ 𝑤)))
144	143	sseq1d 3948	. . . . . . . . 9 ⊢ (𝑠 = (𝑧 ∩ 𝑤) → ((𝐹 “ 𝑠) ⊆ 𝑡 ↔ (𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡))
145	144	imbi1d 341	. . . . . . . 8 ⊢ (𝑠 = (𝑧 ∩ 𝑤) → (((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)) ↔ ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
146	142, 145	syl5ibrcom 247	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) → (𝑠 = (𝑧 ∩ 𝑤) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
147	146	rexlimdvva 3192	. . . . . 6 ⊢ (𝜑 → (∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))𝑠 = (𝑧 ∩ 𝑤) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
148	48, 55, 147	3jaod 1432	. . . . 5 ⊢ (𝜑 → ((𝑠 ∈ (fi‘𝐵) ∨ 𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∨ ∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))𝑠 = (𝑧 ∩ 𝑤)) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
149	46, 148	sylbid 240	. . . 4 ⊢ (𝜑 → (𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
150	149	rexlimdv 3134	. . 3 ⊢ (𝜑 → (∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))
151	150	impcomd 411	. 2 ⊢ (𝜑 → ((𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡) → 𝑡 ∈ 𝐿))
152	44, 151	impbid 212	1 ⊢ (𝜑 → (𝑡 ∈ 𝐿 ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ w3o 1086   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∃wrex 3059  Vcvv 3427   ∪ cun 3883   ∩ cin 3884   ⊆ wss 3885   ↦ cmpt 5155  ^◡ccnv 5619  dom cdm 5620  ran crn 5621   “ cima 5623  Fun wfun 6481  ⟶wf 6483  ‘cfv 6487  (class class class)co 7356  ficfi 9312  fBascfbas 21329  filGencfg 21330  Filcfil 23798   FilMap cfm 23886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2184  ax-ext 2707  ax-rep 5201  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3060  df-reu 3341  df-rab 3388  df-v 3429  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-int 4880  df-iun 4925  df-br 5075  df-opab 5137  df-mpt 5156  df-tr 5182  df-id 5515  df-eprel 5520  df-po 5528  df-so 5529  df-fr 5573  df-we 5575  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-ord 6315  df-on 6316  df-lim 6317  df-suc 6318  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-1o 8394  df-2o 8395  df-en 8883  df-fin 8886  df-fi 9313  df-fbas 21338  df-fg 21339  df-fil 23799  df-fm 23891

This theorem is referenced by:  fmfnfm  23911