fmfnfmlem4 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fmfnfmlem4		Structured version Visualization version GIF version

Theorem fmfnfmlem4 21761

Description: Lemma for fmfnfm 21762. (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 21656	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑡 ∈ 𝐿) → 𝑡 ⊆ 𝑋)
3	2	ex 450	. . . 4 ⊢ (𝐿 ∈ (Fil‘𝑋) → (𝑡 ∈ 𝐿 → 𝑡 ⊆ 𝑋))
4	1, 3	syl 17	. . 3 ⊢ (𝜑 → (𝑡 ∈ 𝐿 → 𝑡 ⊆ 𝑋))
5		fmfnfm.b	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌))
6		mptexg 6484	. . . . . . . . . . 11 ⊢ (𝐿 ∈ (Fil‘𝑋) → (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ V)
7		rnexg 7098	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ V → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ V)
8	6, 7	syl 17	. . . . . . . . . 10 ⊢ (𝐿 ∈ (Fil‘𝑋) → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ V)
9	1, 8	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ V)
10		unexg 6959	. . . . . . . . 9 ⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ V) → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ∈ V)
11	5, 9, 10	syl2anc 693	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ∈ V)
12		ssfii 8325	. . . . . . . . 9 ⊢ ((𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ∈ V → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))
13	12	unssbd 3791	. . . . . . . 8 ⊢ ((𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ∈ V → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))
14	11, 13	syl 17	. . . . . . 7 ⊢ (𝜑 → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))
15	14	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))
16		eqid 2622	. . . . . . . . 9 ⊢ (^◡𝐹 “ 𝑡) = (^◡𝐹 “ 𝑡)
17		imaeq2 5462	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑡 → (^◡𝐹 “ 𝑥) = (^◡𝐹 “ 𝑡))
18	17	eqeq2d 2632	. . . . . . . . . 10 ⊢ (𝑥 = 𝑡 → ((^◡𝐹 “ 𝑡) = (^◡𝐹 “ 𝑥) ↔ (^◡𝐹 “ 𝑡) = (^◡𝐹 “ 𝑡)))
19	18	rspcev 3309	. . . . . . . . 9 ⊢ ((𝑡 ∈ 𝐿 ∧ (^◡𝐹 “ 𝑡) = (^◡𝐹 “ 𝑡)) → ∃𝑥 ∈ 𝐿 (^◡𝐹 “ 𝑡) = (^◡𝐹 “ 𝑥))
20	16, 19	mpan2 707	. . . . . . . 8 ⊢ (𝑡 ∈ 𝐿 → ∃𝑥 ∈ 𝐿 (^◡𝐹 “ 𝑡) = (^◡𝐹 “ 𝑥))
21	20	adantl 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → ∃𝑥 ∈ 𝐿 (^◡𝐹 “ 𝑡) = (^◡𝐹 “ 𝑥))
22		elfvdm 6220	. . . . . . . . . . 11 ⊢ (𝐵 ∈ (fBas‘𝑌) → 𝑌 ∈ dom fBas)
23	5, 22	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ dom fBas)
24		cnvimass 5485	. . . . . . . . . . 11 ⊢ (^◡𝐹 “ 𝑡) ⊆ dom 𝐹
25		fmfnfm.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝑌⟶𝑋)
26		fdm 6051	. . . . . . . . . . . 12 ⊢ (𝐹:𝑌⟶𝑋 → dom 𝐹 = 𝑌)
27	25, 26	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝐹 = 𝑌)
28	24, 27	syl5sseq 3653	. . . . . . . . . 10 ⊢ (𝜑 → (^◡𝐹 “ 𝑡) ⊆ 𝑌)
29	23, 28	ssexd 4805	. . . . . . . . 9 ⊢ (𝜑 → (^◡𝐹 “ 𝑡) ∈ V)
30	29	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → (^◡𝐹 “ 𝑡) ∈ V)
31		eqid 2622	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) = (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))
32	31	elrnmpt 5372	. . . . . . . 8 ⊢ ((^◡𝐹 “ 𝑡) ∈ V → ((^◡𝐹 “ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (^◡𝐹 “ 𝑡) = (^◡𝐹 “ 𝑥)))
33	30, 32	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → ((^◡𝐹 “ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (^◡𝐹 “ 𝑡) = (^◡𝐹 “ 𝑥)))
34	21, 33	mpbird 247	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → (^◡𝐹 “ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
35	15, 34	sseldd 3604	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → (^◡𝐹 “ 𝑡) ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))
36		ffun 6048	. . . . . . . 8 ⊢ (𝐹:𝑌⟶𝑋 → Fun 𝐹)
37		ssid 3624	. . . . . . . 8 ⊢ (^◡𝐹 “ 𝑡) ⊆ (^◡𝐹 “ 𝑡)
38		funimass2 5972	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ (^◡𝐹 “ 𝑡) ⊆ (^◡𝐹 “ 𝑡)) → (𝐹 “ (^◡𝐹 “ 𝑡)) ⊆ 𝑡)
39	36, 37, 38	sylancl 694	. . . . . . 7 ⊢ (𝐹:𝑌⟶𝑋 → (𝐹 “ (^◡𝐹 “ 𝑡)) ⊆ 𝑡)
40	25, 39	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐹 “ (^◡𝐹 “ 𝑡)) ⊆ 𝑡)
41	40	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → (𝐹 “ (^◡𝐹 “ 𝑡)) ⊆ 𝑡)
42		imaeq2 5462	. . . . . . 7 ⊢ (𝑠 = (^◡𝐹 “ 𝑡) → (𝐹 “ 𝑠) = (𝐹 “ (^◡𝐹 “ 𝑡)))
43	42	sseq1d 3632	. . . . . 6 ⊢ (𝑠 = (^◡𝐹 “ 𝑡) → ((𝐹 “ 𝑠) ⊆ 𝑡 ↔ (𝐹 “ (^◡𝐹 “ 𝑡)) ⊆ 𝑡))
44	43	rspcev 3309	. . . . 5 ⊢ (((^◡𝐹 “ 𝑡) ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ∧ (𝐹 “ (^◡𝐹 “ 𝑡)) ⊆ 𝑡) → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡)
45	35, 41, 44	syl2anc 693	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐿) → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡)
46	45	ex 450	. . 3 ⊢ (𝜑 → (𝑡 ∈ 𝐿 → ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡))
47	4, 46	jcad 555	. 2 ⊢ (𝜑 → (𝑡 ∈ 𝐿 → (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡)))
48		elfiun 8336	. . . . . . 7 ⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ V) → (𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ↔ (𝑠 ∈ (fi‘𝐵) ∨ 𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ∨ ∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))𝑠 = (𝑧 ∩ 𝑤))))
49	5, 9, 48	syl2anc 693	. . . . . 6 ⊢ (𝜑 → (𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ↔ (𝑠 ∈ (fi‘𝐵) ∨ 𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ∨ ∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))𝑠 = (𝑧 ∩ 𝑤))))
50		fmfnfm.fm	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)
51	5, 1, 25, 50	fmfnfmlem1 21758	. . . . . . 7 ⊢ (𝜑 → (𝑠 ∈ (fi‘𝐵) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
52	5, 1, 25, 50	fmfnfmlem3 21760	. . . . . . . . 9 ⊢ (𝜑 → (fi‘ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) = ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
53	52	eleq2d 2687	. . . . . . . 8 ⊢ (𝜑 → (𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ↔ 𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))
54		vex 3203	. . . . . . . . . 10 ⊢ 𝑠 ∈ V
55	31	elrnmpt 5372	. . . . . . . . . 10 ⊢ (𝑠 ∈ V → (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑥)))
56	54, 55	ax-mp 5	. . . . . . . . 9 ⊢ (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑥))
57	5, 1, 25, 50	fmfnfmlem2 21759	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑥 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
58	56, 57	syl5bi 232	. . . . . . . 8 ⊢ (𝜑 → (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
59	53, 58	sylbid 230	. . . . . . 7 ⊢ (𝜑 → (𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
60	52	eleq2d 2687	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ↔ 𝑤 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))
61		vex 3203	. . . . . . . . . . . . . 14 ⊢ 𝑤 ∈ V
62	31	elrnmpt 5372	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ V → (𝑤 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑤 = (^◡𝐹 “ 𝑥)))
63	61, 62	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑤 = (^◡𝐹 “ 𝑥))
64	60, 63	syl6bb 276	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ↔ ∃𝑥 ∈ 𝐿 𝑤 = (^◡𝐹 “ 𝑥)))
65	64	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (fi‘𝐵)) → (𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ↔ ∃𝑥 ∈ 𝐿 𝑤 = (^◡𝐹 “ 𝑥)))
66		fbssfi 21641	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑧 ∈ (fi‘𝐵)) → ∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧)
67	5, 66	sylan 488	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (fi‘𝐵)) → ∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧)
68	1	ad3antrrr 766	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝐿 ∈ (Fil‘𝑋))
69	1	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → 𝐿 ∈ (Fil‘𝑋))
70	50	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)
71		filtop 21659	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐿 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐿)
72	1, 71	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑋 ∈ 𝐿)
73	72, 5, 25	3jca 1242	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋))
74	73	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋))
75		ssfg 21676	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ (𝑌filGen𝐵))
76	5, 75	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐵 ⊆ (𝑌filGen𝐵))
77	76	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈ (𝑌filGen𝐵))
78		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑌filGen𝐵) = (𝑌filGen𝐵)
79	78	imaelfm 21755	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑠 ∈ (𝑌filGen𝐵)) → (𝐹 “ 𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
80	74, 77, 79	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝐹 “ 𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
81	70, 80	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝐹 “ 𝑠) ∈ 𝐿)
82	81	adantrr 753	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → (𝐹 “ 𝑠) ∈ 𝐿)
83	69, 82	jca 554	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → (𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿))
84		filin 21658	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿 ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿)
85	84	3expa 1265	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿)
86	83, 85	sylan 488	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿)
87	86	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿)
88		simprr 796	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝑡 ⊆ 𝑋)
89		elin 3796	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) ↔ (𝑤 ∈ (𝐹 “ 𝑠) ∧ 𝑤 ∈ 𝑥))
90	25, 36	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → Fun 𝐹)
91		fvelima 6248	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Fun 𝐹 ∧ 𝑤 ∈ (𝐹 “ 𝑠)) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑤)
92	91	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Fun 𝐹 → (𝑤 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑤))
93	90, 92	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑤 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑤))
94	93	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → (𝑤 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑤))
95	90	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → Fun 𝐹)
96		simplrr 801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) → 𝑠 ⊆ 𝑧)
97		simprl 794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥)) → 𝑦 ∈ 𝑠)
98		ssel2 3598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑠 ⊆ 𝑧 ∧ 𝑦 ∈ 𝑠) → 𝑦 ∈ 𝑧)
99	96, 97, 98	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → 𝑦 ∈ 𝑧)
100	90	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝑠) → Fun 𝐹)
101		fbelss 21637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ 𝑌)
102	5, 101	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ 𝑌)
103	27	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → dom 𝐹 = 𝑌)
104	102, 103	sseqtr4d 3642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ dom 𝐹)
105	104	adantrr 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → 𝑠 ⊆ dom 𝐹)
106	105	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝑠) → 𝑦 ∈ dom 𝐹)
107		fvimacnv 6332	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹) → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑦 ∈ (^◡𝐹 “ 𝑥)))
108	100, 106, 107	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑦 ∈ (^◡𝐹 “ 𝑥)))
109	108	biimpd 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 → 𝑦 ∈ (^◡𝐹 “ 𝑥)))
110	109	impr 649	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥)) → 𝑦 ∈ (^◡𝐹 “ 𝑥))
111	110	ad2ant2rl 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → 𝑦 ∈ (^◡𝐹 “ 𝑥))
112	99, 111	elind 3798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → 𝑦 ∈ (𝑧 ∩ (^◡𝐹 “ 𝑥)))
113		inss2 3834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 ∩ (^◡𝐹 “ 𝑥)) ⊆ (^◡𝐹 “ 𝑥)
114		cnvimass 5485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (^◡𝐹 “ 𝑥) ⊆ dom 𝐹
115	113, 114	sstri 3612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 ∩ (^◡𝐹 “ 𝑥)) ⊆ dom 𝐹
116		funfvima2 6493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((Fun 𝐹 ∧ (𝑧 ∩ (^◡𝐹 “ 𝑥)) ⊆ dom 𝐹) → (𝑦 ∈ (𝑧 ∩ (^◡𝐹 “ 𝑥)) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥)))))
117	115, 116	mpan2 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (Fun 𝐹 → (𝑦 ∈ (𝑧 ∩ (^◡𝐹 “ 𝑥)) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥)))))
118	95, 112, 117	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ (𝑡 ⊆ 𝑋 ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥))) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥))))
119	118	anassrs 680	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) ∧ (𝑦 ∈ 𝑠 ∧ (𝐹‘𝑦) ∈ 𝑥)) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥))))
120	119	expr 643	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥)))))
121		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹‘𝑦) = 𝑤 → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑤 ∈ 𝑥))
122		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹‘𝑦) = 𝑤 → ((𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥))) ↔ 𝑤 ∈ (𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥)))))
123	121, 122	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹‘𝑦) = 𝑤 → (((𝐹‘𝑦) ∈ 𝑥 → (𝐹‘𝑦) ∈ (𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥)))) ↔ (𝑤 ∈ 𝑥 → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥))))))
124	120, 123	syl5ibcom 235	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) = 𝑤 → (𝑤 ∈ 𝑥 → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥))))))
125	124	rexlimdva 3031	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → (∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑤 → (𝑤 ∈ 𝑥 → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥))))))
126	94, 125	syld 47	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → (𝑤 ∈ (𝐹 “ 𝑠) → (𝑤 ∈ 𝑥 → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥))))))
127	126	impd 447	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → ((𝑤 ∈ (𝐹 “ 𝑠) ∧ 𝑤 ∈ 𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥)))))
128	89, 127	syl5bi 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ 𝑡 ⊆ 𝑋) → (𝑤 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥)))))
129	128	adantrl 752	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝑤 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) → 𝑤 ∈ (𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥)))))
130	129	ssrdv 3609	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ((𝐹 “ 𝑠) ∩ 𝑥) ⊆ (𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥))))
131		simprl 794	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥))) ⊆ 𝑡)
132	130, 131	sstrd 3613	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ((𝐹 “ 𝑠) ∩ 𝑥) ⊆ 𝑡)
133		filss 21657	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ (((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿 ∧ 𝑡 ⊆ 𝑋 ∧ ((𝐹 “ 𝑠) ∩ 𝑥) ⊆ 𝑡)) → 𝑡 ∈ 𝐿)
134	68, 87, 88, 132, 133	syl13anc 1328	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥))) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝑡 ∈ 𝐿)
135	134	exp32 631	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥))) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))
136		ineq2 3808	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (^◡𝐹 “ 𝑥) → (𝑧 ∩ 𝑤) = (𝑧 ∩ (^◡𝐹 “ 𝑥)))
137	136	imaeq2d 5466	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = (^◡𝐹 “ 𝑥) → (𝐹 “ (𝑧 ∩ 𝑤)) = (𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥))))
138	137	sseq1d 3632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = (^◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 ↔ (𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥))) ⊆ 𝑡))
139	138	imbi1d 331	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = (^◡𝐹 “ 𝑥) → (((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)) ↔ ((𝐹 “ (𝑧 ∩ (^◡𝐹 “ 𝑥))) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
140	135, 139	syl5ibrcom 237	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) ∧ 𝑥 ∈ 𝐿) → (𝑤 = (^◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
141	140	rexlimdva 3031	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑠 ∈ 𝐵 ∧ 𝑠 ⊆ 𝑧)) → (∃𝑥 ∈ 𝐿 𝑤 = (^◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
142	141	rexlimdvaa 3032	. . . . . . . . . . . . 13 ⊢ (𝜑 → (∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧 → (∃𝑥 ∈ 𝐿 𝑤 = (^◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))))
143	142	imp 445	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑧) → (∃𝑥 ∈ 𝐿 𝑤 = (^◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
144	67, 143	syldan 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (fi‘𝐵)) → (∃𝑥 ∈ 𝐿 𝑤 = (^◡𝐹 “ 𝑥) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
145	65, 144	sylbid 230	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (fi‘𝐵)) → (𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
146	145	impr 649	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) → ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))
147		imaeq2 5462	. . . . . . . . . . 11 ⊢ (𝑠 = (𝑧 ∩ 𝑤) → (𝐹 “ 𝑠) = (𝐹 “ (𝑧 ∩ 𝑤)))
148	147	sseq1d 3632	. . . . . . . . . 10 ⊢ (𝑠 = (𝑧 ∩ 𝑤) → ((𝐹 “ 𝑠) ⊆ 𝑡 ↔ (𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡))
149	148	imbi1d 331	. . . . . . . . 9 ⊢ (𝑠 = (𝑧 ∩ 𝑤) → (((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)) ↔ ((𝐹 “ (𝑧 ∩ 𝑤)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
150	146, 149	syl5ibrcom 237	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) → (𝑠 = (𝑧 ∩ 𝑤) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
151	150	rexlimdvva 3038	. . . . . . 7 ⊢ (𝜑 → (∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))𝑠 = (𝑧 ∩ 𝑤) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
152	51, 59, 151	3jaod 1392	. . . . . 6 ⊢ (𝜑 → ((𝑠 ∈ (fi‘𝐵) ∨ 𝑠 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ∨ ∃𝑧 ∈ (fi‘𝐵)∃𝑤 ∈ (fi‘ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))𝑠 = (𝑧 ∩ 𝑤)) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
153	49, 152	sylbid 230	. . . . 5 ⊢ (𝜑 → (𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
154	153	rexlimdv 3030	. . . 4 ⊢ (𝜑 → (∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))
155	154	com23 86	. . 3 ⊢ (𝜑 → (𝑡 ⊆ 𝑋 → (∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡 → 𝑡 ∈ 𝐿)))
156	155	impd 447	. 2 ⊢ (𝜑 → ((𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡) → 𝑡 ∈ 𝐿))
157	47, 156	impbid 202	1 ⊢ (𝜑 → (𝑡 ∈ 𝐿 ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∨ w3o 1036 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ∃wrex 2913 Vcvv 3200 ∪ cun 3572 ∩ cin 3573 ⊆ wss 3574 ↦ cmpt 4729 ^◡ccnv 5113 dom cdm 5114 ran crn 5115 “ cima 5117 Fun wfun 5882 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 ficfi 8316 fBascfbas 19734 filGencfg 19735 Filcfil 21649 FilMap cfm 21737

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-fin 7959 df-fi 8317 df-fbas 19743 df-fg 19744 df-fil 21650 df-fm 21742

This theorem is referenced by: fmfnfm 21762

W3C validator