Theorem rnelfmlem 22249

Description: Lemma for rnelfm 22250. (Contributed by Jeff Hankins, 14-Nov-2009.)

Assertion

Ref	Expression
rnelfmlem	⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐹   𝑥,𝐿   𝑥,𝑋   𝑥,𝑌

Proof of Theorem rnelfmlem

Dummy variables 𝑟 𝑠 𝑡 𝑢 𝑣 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl1 1184	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝑌 ∈ 𝐴)
2		cnvimass 5830	. . . . . . 7 ⊢ (◡𝐹 “ 𝑥) ⊆ dom 𝐹
3		simpl3 1186	. . . . . . 7 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝐹:𝑌⟶𝑋)
4	2, 3	fssdm 6403	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (◡𝐹 “ 𝑥) ⊆ 𝑌)
5	1, 4	sselpwd 5126	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (◡𝐹 “ 𝑥) ∈ 𝒫 𝑌)
6	5	adantr 481	. . . 4 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → (◡𝐹 “ 𝑥) ∈ 𝒫 𝑌)
7	6	fmpttd 6747	. . 3 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)):𝐿⟶𝒫 𝑌)
8	7	frnd 6394	. 2 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ⊆ 𝒫 𝑌)
9		filtop 22152	. . . . . . . 8 ⊢ (𝐿 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐿)
10	9	3ad2ant2 1127	. . . . . . 7 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → 𝑋 ∈ 𝐿)
11	10	adantr 481	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝑋 ∈ 𝐿)
12		fimacnv 6709	. . . . . . . . 9 ⊢ (𝐹:𝑌⟶𝑋 → (◡𝐹 “ 𝑋) = 𝑌)
13	12	eqcomd 2801	. . . . . . . 8 ⊢ (𝐹:𝑌⟶𝑋 → 𝑌 = (◡𝐹 “ 𝑋))
14	13	3ad2ant3 1128	. . . . . . 7 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → 𝑌 = (◡𝐹 “ 𝑋))
15	14	adantr 481	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝑌 = (◡𝐹 “ 𝑋))
16		imaeq2 5807	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (◡𝐹 “ 𝑥) = (◡𝐹 “ 𝑋))
17	16	rspceeqv 3577	. . . . . 6 ⊢ ((𝑋 ∈ 𝐿 ∧ 𝑌 = (◡𝐹 “ 𝑋)) → ∃𝑥 ∈ 𝐿 𝑌 = (◡𝐹 “ 𝑥))
18	11, 15, 17	syl2anc 584	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ∃𝑥 ∈ 𝐿 𝑌 = (◡𝐹 “ 𝑥))
19		eqid 2795	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) = (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))
20	19	elrnmpt 5715	. . . . . . 7 ⊢ (𝑌 ∈ 𝐴 → (𝑌 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑌 = (◡𝐹 “ 𝑥)))
21	20	3ad2ant1 1126	. . . . . 6 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (𝑌 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑌 = (◡𝐹 “ 𝑥)))
22	21	adantr 481	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (𝑌 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑌 = (◡𝐹 “ 𝑥)))
23	18, 22	mpbird 258	. . . 4 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝑌 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))
24	23	ne0d 4225	. . 3 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ≠ ∅)
25		0nelfil 22146	. . . . . . 7 ⊢ (𝐿 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝐿)
26	25	3ad2ant2 1127	. . . . . 6 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → ¬ ∅ ∈ 𝐿)
27	26	adantr 481	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ¬ ∅ ∈ 𝐿)
28		0ex 5107	. . . . . . 7 ⊢ ∅ ∈ V
29	19	elrnmpt 5715	. . . . . . 7 ⊢ (∅ ∈ V → (∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 ∅ = (◡𝐹 “ 𝑥)))
30	28, 29	ax-mp 5	. . . . . 6 ⊢ (∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 ∅ = (◡𝐹 “ 𝑥))
31		ffn 6387	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹:𝑌⟶𝑋 → 𝐹 Fn 𝑌)
32		fvelrnb 6599	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Fn 𝑌 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦))
33	31, 32	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑌⟶𝑋 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦))
34	33	3ad2ant3 1128	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦))
35	34	ad2antrr 722	. . . . . . . . . . . . . . 15 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦))
36		eleq1 2870	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑧) = 𝑦 → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑦 ∈ 𝑥))
37	36	biimparc 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝐹‘𝑧) = 𝑦) → (𝐹‘𝑧) ∈ 𝑥)
38	37	ad2ant2l 742	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → (𝐹‘𝑧) ∈ 𝑥)
39	38	adantll 710	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → (𝐹‘𝑧) ∈ 𝑥)
40		ffun 6390	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:𝑌⟶𝑋 → Fun 𝐹)
41	40	3ad2ant3 1128	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → Fun 𝐹)
42	41	ad3antrrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → Fun 𝐹)
43		fdm 6395	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹:𝑌⟶𝑋 → dom 𝐹 = 𝑌)
44	43	eleq2d 2868	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:𝑌⟶𝑋 → (𝑧 ∈ dom 𝐹 ↔ 𝑧 ∈ 𝑌))
45	44	biimpar 478	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:𝑌⟶𝑋 ∧ 𝑧 ∈ 𝑌) → 𝑧 ∈ dom 𝐹)
46	45	3ad2antl3 1180	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑧 ∈ 𝑌) → 𝑧 ∈ dom 𝐹)
47	46	adantlr 711	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑧 ∈ 𝑌) → 𝑧 ∈ dom 𝐹)
48	47	ad2ant2r 743	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → 𝑧 ∈ dom 𝐹)
49		fvimacnv 6693	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐹 ∧ 𝑧 ∈ dom 𝐹) → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑧 ∈ (◡𝐹 “ 𝑥)))
50	42, 48, 49	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑧 ∈ (◡𝐹 “ 𝑥)))
51	39, 50	mpbid 233	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → 𝑧 ∈ (◡𝐹 “ 𝑥))
52		n0i 4223	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (◡𝐹 “ 𝑥) → ¬ (◡𝐹 “ 𝑥) = ∅)
53		eqcom 2802	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝐹 “ 𝑥) = ∅ ↔ ∅ = (◡𝐹 “ 𝑥))
54	52, 53	sylnib 329	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (◡𝐹 “ 𝑥) → ¬ ∅ = (◡𝐹 “ 𝑥))
55	51, 54	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → ¬ ∅ = (◡𝐹 “ 𝑥))
56	55	rexlimdvaa 3248	. . . . . . . . . . . . . . 15 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) → (∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦 → ¬ ∅ = (◡𝐹 “ 𝑥)))
57	35, 56	sylbid 241	. . . . . . . . . . . . . 14 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) → (𝑦 ∈ ran 𝐹 → ¬ ∅ = (◡𝐹 “ 𝑥)))
58	57	con2d 136	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) → (∅ = (◡𝐹 “ 𝑥) → ¬ 𝑦 ∈ ran 𝐹))
59	58	expr 457	. . . . . . . . . . . 12 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → (𝑦 ∈ 𝑥 → (∅ = (◡𝐹 “ 𝑥) → ¬ 𝑦 ∈ ran 𝐹)))
60	59	com23 86	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → (∅ = (◡𝐹 “ 𝑥) → (𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹)))
61	60	impr 455	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (◡𝐹 “ 𝑥))) → (𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹))
62	61	alrimiv 1905	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (◡𝐹 “ 𝑥))) → ∀𝑦(𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹))
63		imnan 400	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ¬ (𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹))
64		elin 4094	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝑥 ∩ ran 𝐹) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹))
65	63, 64	xchbinxr 336	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
66	65	albii 1801	. . . . . . . . . 10 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ∀𝑦 ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
67		eq0 4232	. . . . . . . . . 10 ⊢ ((𝑥 ∩ ran 𝐹) = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
68		eqcom 2802	. . . . . . . . . 10 ⊢ ((𝑥 ∩ ran 𝐹) = ∅ ↔ ∅ = (𝑥 ∩ ran 𝐹))
69	66, 67, 68	3bitr2i 300	. . . . . . . . 9 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ∅ = (𝑥 ∩ ran 𝐹))
70	62, 69	sylib 219	. . . . . . . 8 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (◡𝐹 “ 𝑥))) → ∅ = (𝑥 ∩ ran 𝐹))
71		simpll2 1206	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (◡𝐹 “ 𝑥))) → 𝐿 ∈ (Fil‘𝑋))
72		simprl 767	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (◡𝐹 “ 𝑥))) → 𝑥 ∈ 𝐿)
73		simplr 765	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (◡𝐹 “ 𝑥))) → ran 𝐹 ∈ 𝐿)
74		filin 22151	. . . . . . . . 9 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝐿 ∧ ran 𝐹 ∈ 𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
75	71, 72, 73, 74	syl3anc 1364	. . . . . . . 8 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (◡𝐹 “ 𝑥))) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
76	70, 75	eqeltrd 2883	. . . . . . 7 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (◡𝐹 “ 𝑥))) → ∅ ∈ 𝐿)
77	76	rexlimdvaa 3248	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (∃𝑥 ∈ 𝐿 ∅ = (◡𝐹 “ 𝑥) → ∅ ∈ 𝐿))
78	30, 77	syl5bi 243	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) → ∅ ∈ 𝐿))
79	27, 78	mtod 199	. . . 4 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ¬ ∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))
80		df-nel 3091	. . . 4 ⊢ (∅ ∉ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ¬ ∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))
81	79, 80	sylibr 235	. . 3 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ∅ ∉ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))
82	19	elrnmpt 5715	. . . . . . . . 9 ⊢ (𝑟 ∈ V → (𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑟 = (◡𝐹 “ 𝑥)))
83	82	elv 3442	. . . . . . . 8 ⊢ (𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑟 = (◡𝐹 “ 𝑥))
84		imaeq2 5807	. . . . . . . . . 10 ⊢ (𝑥 = 𝑢 → (◡𝐹 “ 𝑥) = (◡𝐹 “ 𝑢))
85	84	eqeq2d 2805	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → (𝑟 = (◡𝐹 “ 𝑥) ↔ 𝑟 = (◡𝐹 “ 𝑢)))
86	85	cbvrexv 3404	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐿 𝑟 = (◡𝐹 “ 𝑥) ↔ ∃𝑢 ∈ 𝐿 𝑟 = (◡𝐹 “ 𝑢))
87	83, 86	bitri 276	. . . . . . 7 ⊢ (𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑢 ∈ 𝐿 𝑟 = (◡𝐹 “ 𝑢))
88	19	elrnmpt 5715	. . . . . . . . 9 ⊢ (𝑠 ∈ V → (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥)))
89	88	elv 3442	. . . . . . . 8 ⊢ (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥))
90		imaeq2 5807	. . . . . . . . . 10 ⊢ (𝑥 = 𝑣 → (◡𝐹 “ 𝑥) = (◡𝐹 “ 𝑣))
91	90	eqeq2d 2805	. . . . . . . . 9 ⊢ (𝑥 = 𝑣 → (𝑠 = (◡𝐹 “ 𝑥) ↔ 𝑠 = (◡𝐹 “ 𝑣)))
92	91	cbvrexv 3404	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥) ↔ ∃𝑣 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑣))
93	89, 92	bitri 276	. . . . . . 7 ⊢ (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑣 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑣))
94	87, 93	anbi12i 626	. . . . . 6 ⊢ ((𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∧ 𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ↔ (∃𝑢 ∈ 𝐿 𝑟 = (◡𝐹 “ 𝑢) ∧ ∃𝑣 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑣)))
95		reeanv 3328	. . . . . 6 ⊢ (∃𝑢 ∈ 𝐿 ∃𝑣 ∈ 𝐿 (𝑟 = (◡𝐹 “ 𝑢) ∧ 𝑠 = (◡𝐹 “ 𝑣)) ↔ (∃𝑢 ∈ 𝐿 𝑟 = (◡𝐹 “ 𝑢) ∧ ∃𝑣 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑣)))
96	94, 95	bitr4i 279	. . . . 5 ⊢ ((𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∧ 𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ↔ ∃𝑢 ∈ 𝐿 ∃𝑣 ∈ 𝐿 (𝑟 = (◡𝐹 “ 𝑢) ∧ 𝑠 = (◡𝐹 “ 𝑣)))
97		filin 22151	. . . . . . . . . . . . . 14 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) → (𝑢 ∩ 𝑣) ∈ 𝐿)
98	97	3expb 1113	. . . . . . . . . . . . 13 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → (𝑢 ∩ 𝑣) ∈ 𝐿)
99	98	adantlr 711	. . . . . . . . . . . 12 ⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → (𝑢 ∩ 𝑣) ∈ 𝐿)
100		eqidd 2796	. . . . . . . . . . . 12 ⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → (◡𝐹 “ (𝑢 ∩ 𝑣)) = (◡𝐹 “ (𝑢 ∩ 𝑣)))
101		imaeq2 5807	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑢 ∩ 𝑣) → (◡𝐹 “ 𝑥) = (◡𝐹 “ (𝑢 ∩ 𝑣)))
102	101	rspceeqv 3577	. . . . . . . . . . . 12 ⊢ (((𝑢 ∩ 𝑣) ∈ 𝐿 ∧ (◡𝐹 “ (𝑢 ∩ 𝑣)) = (◡𝐹 “ (𝑢 ∩ 𝑣))) → ∃𝑥 ∈ 𝐿 (◡𝐹 “ (𝑢 ∩ 𝑣)) = (◡𝐹 “ 𝑥))
103	99, 100, 102	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → ∃𝑥 ∈ 𝐿 (◡𝐹 “ (𝑢 ∩ 𝑣)) = (◡𝐹 “ 𝑥))
104	103	3adantl1 1159	. . . . . . . . . 10 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → ∃𝑥 ∈ 𝐿 (◡𝐹 “ (𝑢 ∩ 𝑣)) = (◡𝐹 “ 𝑥))
105	104	ad2ant2r 743	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (◡𝐹 “ 𝑢) ∧ 𝑠 = (◡𝐹 “ 𝑣)))) → ∃𝑥 ∈ 𝐿 (◡𝐹 “ (𝑢 ∩ 𝑣)) = (◡𝐹 “ 𝑥))
106		simpll1 1205	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (◡𝐹 “ 𝑢) ∧ 𝑠 = (◡𝐹 “ 𝑣)))) → 𝑌 ∈ 𝐴)
107		cnvimass 5830	. . . . . . . . . . . . . 14 ⊢ (◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ dom 𝐹
108	107, 43	sseqtrid 3944	. . . . . . . . . . . . 13 ⊢ (𝐹:𝑌⟶𝑋 → (◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ 𝑌)
109	108	3ad2ant3 1128	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ 𝑌)
110	109	ad2antrr 722	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (◡𝐹 “ 𝑢) ∧ 𝑠 = (◡𝐹 “ 𝑣)))) → (◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ 𝑌)
111	106, 110	ssexd 5124	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (◡𝐹 “ 𝑢) ∧ 𝑠 = (◡𝐹 “ 𝑣)))) → (◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ V)
112	19	elrnmpt 5715	. . . . . . . . . 10 ⊢ ((◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ V → ((◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (◡𝐹 “ (𝑢 ∩ 𝑣)) = (◡𝐹 “ 𝑥)))
113	111, 112	syl 17	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (◡𝐹 “ 𝑢) ∧ 𝑠 = (◡𝐹 “ 𝑣)))) → ((◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (◡𝐹 “ (𝑢 ∩ 𝑣)) = (◡𝐹 “ 𝑥)))
114	105, 113	mpbird 258	. . . . . . . 8 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (◡𝐹 “ 𝑢) ∧ 𝑠 = (◡𝐹 “ 𝑣)))) → (◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))
115		simprrl 777	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (◡𝐹 “ 𝑢) ∧ 𝑠 = (◡𝐹 “ 𝑣)))) → 𝑟 = (◡𝐹 “ 𝑢))
116		simprrr 778	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (◡𝐹 “ 𝑢) ∧ 𝑠 = (◡𝐹 “ 𝑣)))) → 𝑠 = (◡𝐹 “ 𝑣))
117	115, 116	ineq12d 4114	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (◡𝐹 “ 𝑢) ∧ 𝑠 = (◡𝐹 “ 𝑣)))) → (𝑟 ∩ 𝑠) = ((◡𝐹 “ 𝑢) ∩ (◡𝐹 “ 𝑣)))
118		funcnvcnv 6296	. . . . . . . . . . . . 13 ⊢ (Fun 𝐹 → Fun ◡◡𝐹)
119		imain 6314	. . . . . . . . . . . . 13 ⊢ (Fun ◡◡𝐹 → (◡𝐹 “ (𝑢 ∩ 𝑣)) = ((◡𝐹 “ 𝑢) ∩ (◡𝐹 “ 𝑣)))
120	40, 118, 119	3syl 18	. . . . . . . . . . . 12 ⊢ (𝐹:𝑌⟶𝑋 → (◡𝐹 “ (𝑢 ∩ 𝑣)) = ((◡𝐹 “ 𝑢) ∩ (◡𝐹 “ 𝑣)))
121	120	3ad2ant3 1128	. . . . . . . . . . 11 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (◡𝐹 “ (𝑢 ∩ 𝑣)) = ((◡𝐹 “ 𝑢) ∩ (◡𝐹 “ 𝑣)))
122	121	ad2antrr 722	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (◡𝐹 “ 𝑢) ∧ 𝑠 = (◡𝐹 “ 𝑣)))) → (◡𝐹 “ (𝑢 ∩ 𝑣)) = ((◡𝐹 “ 𝑢) ∩ (◡𝐹 “ 𝑣)))
123	117, 122	eqtr4d 2834	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (◡𝐹 “ 𝑢) ∧ 𝑠 = (◡𝐹 “ 𝑣)))) → (𝑟 ∩ 𝑠) = (◡𝐹 “ (𝑢 ∩ 𝑣)))
124		eqimss2 3949	. . . . . . . . 9 ⊢ ((𝑟 ∩ 𝑠) = (◡𝐹 “ (𝑢 ∩ 𝑣)) → (◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠))
125	123, 124	syl 17	. . . . . . . 8 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (◡𝐹 “ 𝑢) ∧ 𝑠 = (◡𝐹 “ 𝑣)))) → (◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠))
126		sseq1 3917	. . . . . . . . 9 ⊢ (𝑡 = (◡𝐹 “ (𝑢 ∩ 𝑣)) → (𝑡 ⊆ (𝑟 ∩ 𝑠) ↔ (◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠)))
127	126	rspcev 3559	. . . . . . . 8 ⊢ (((◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∧ (◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠)) → ∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠))
128	114, 125, 127	syl2anc 584	. . . . . . 7 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (◡𝐹 “ 𝑢) ∧ 𝑠 = (◡𝐹 “ 𝑣)))) → ∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠))
129	128	exp32 421	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) → ((𝑟 = (◡𝐹 “ 𝑢) ∧ 𝑠 = (◡𝐹 “ 𝑣)) → ∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠))))
130	129	rexlimdvv 3256	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (∃𝑢 ∈ 𝐿 ∃𝑣 ∈ 𝐿 (𝑟 = (◡𝐹 “ 𝑢) ∧ 𝑠 = (◡𝐹 “ 𝑣)) → ∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠)))
131	96, 130	syl5bi 243	. . . 4 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ((𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∧ 𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) → ∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠)))
132	131	ralrimivv 3157	. . 3 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ∀𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))∀𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠))
133	24, 81, 132	3jca 1121	. 2 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ≠ ∅ ∧ ∅ ∉ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∧ ∀𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))∀𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠)))
134		isfbas2 22132	. . 3 ⊢ (𝑌 ∈ 𝐴 → (ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌) ↔ (ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ⊆ 𝒫 𝑌 ∧ (ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ≠ ∅ ∧ ∅ ∉ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∧ ∀𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))∀𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠)))))
135	1, 134	syl 17	. 2 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌) ↔ (ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ⊆ 𝒫 𝑌 ∧ (ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ≠ ∅ ∧ ∅ ∉ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∧ ∀𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))∀𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠)))))
136	8, 133, 135	mpbir2and 709	1 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1080  ∀wal 1520   = wceq 1522   ∈ wcel 2081   ≠ wne 2984   ∉ wnel 3090  ∀wral 3105  ∃wrex 3106  Vcvv 3437   ∩ cin 3862   ⊆ wss 3863  ∅c0 4215  𝒫 cpw 4457   ↦ cmpt 5045  ^◡ccnv 5447  dom cdm 5448  ran crn 5449   “ cima 5451  Fun wfun 6224   Fn wfn 6225  ⟶wf 6226  ‘cfv 6230  fBascfbas 20220  Filcfil 22142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pow 5162  ax-pr 5226

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3710  df-csb 3816  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-pw 4459  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-br 4967  df-opab 5029  df-mpt 5046  df-id 5353  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-res 5460  df-ima 5461  df-iota 6194  df-fun 6232  df-fn 6233  df-f 6234  df-fv 6238  df-fbas 20229  df-fil 22143

This theorem is referenced by:  rnelfm  22250  fmfnfm  22255