rnelfmlem - Metamath Proof Explorer

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

Theorem rnelfmlem 21566

Description: Lemma for rnelfm 21567. (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		simpl3 1059	. . . . . . 7 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝐹:𝑌⟶𝑋)
2		cnvimass 5404	. . . . . . . 8 ⊢ (^◡𝐹 “ 𝑥) ⊆ dom 𝐹
3		fdm 5964	. . . . . . . 8 ⊢ (𝐹:𝑌⟶𝑋 → dom 𝐹 = 𝑌)
4	2, 3	syl5sseq 3616	. . . . . . 7 ⊢ (𝐹:𝑌⟶𝑋 → (^◡𝐹 “ 𝑥) ⊆ 𝑌)
5	1, 4	syl 17	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (^◡𝐹 “ 𝑥) ⊆ 𝑌)
6		simpl1 1057	. . . . . . 7 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝑌 ∈ 𝐴)
7		elpw2g 4754	. . . . . . 7 ⊢ (𝑌 ∈ 𝐴 → ((^◡𝐹 “ 𝑥) ∈ 𝒫 𝑌 ↔ (^◡𝐹 “ 𝑥) ⊆ 𝑌))
8	6, 7	syl 17	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ((^◡𝐹 “ 𝑥) ∈ 𝒫 𝑌 ↔ (^◡𝐹 “ 𝑥) ⊆ 𝑌))
9	5, 8	mpbird 246	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (^◡𝐹 “ 𝑥) ∈ 𝒫 𝑌)
10	9	adantr 480	. . . 4 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → (^◡𝐹 “ 𝑥) ∈ 𝒫 𝑌)
11		eqid 2610	. . . 4 ⊢ (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) = (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))
12	10, 11	fmptd 6292	. . 3 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)):𝐿⟶𝒫 𝑌)
13		frn 5966	. . 3 ⊢ ((𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)):𝐿⟶𝒫 𝑌 → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ⊆ 𝒫 𝑌)
14	12, 13	syl 17	. 2 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ⊆ 𝒫 𝑌)
15		filtop 21469	. . . . . . . 8 ⊢ (𝐿 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐿)
16	15	3ad2ant2 1076	. . . . . . 7 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → 𝑋 ∈ 𝐿)
17	16	adantr 480	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝑋 ∈ 𝐿)
18		fimacnv 6255	. . . . . . . . 9 ⊢ (𝐹:𝑌⟶𝑋 → (^◡𝐹 “ 𝑋) = 𝑌)
19	18	eqcomd 2616	. . . . . . . 8 ⊢ (𝐹:𝑌⟶𝑋 → 𝑌 = (^◡𝐹 “ 𝑋))
20	19	3ad2ant3 1077	. . . . . . 7 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → 𝑌 = (^◡𝐹 “ 𝑋))
21	20	adantr 480	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝑌 = (^◡𝐹 “ 𝑋))
22		imaeq2 5381	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (^◡𝐹 “ 𝑥) = (^◡𝐹 “ 𝑋))
23	22	eqeq2d 2620	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝑌 = (^◡𝐹 “ 𝑥) ↔ 𝑌 = (^◡𝐹 “ 𝑋)))
24	23	rspcev 3282	. . . . . 6 ⊢ ((𝑋 ∈ 𝐿 ∧ 𝑌 = (^◡𝐹 “ 𝑋)) → ∃𝑥 ∈ 𝐿 𝑌 = (^◡𝐹 “ 𝑥))
25	17, 21, 24	syl2anc 691	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ∃𝑥 ∈ 𝐿 𝑌 = (^◡𝐹 “ 𝑥))
26	11	elrnmpt 5293	. . . . . . 7 ⊢ (𝑌 ∈ 𝐴 → (𝑌 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑌 = (^◡𝐹 “ 𝑥)))
27	26	3ad2ant1 1075	. . . . . 6 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (𝑌 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑌 = (^◡𝐹 “ 𝑥)))
28	27	adantr 480	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (𝑌 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑌 = (^◡𝐹 “ 𝑥)))
29	25, 28	mpbird 246	. . . 4 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝑌 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
30		ne0i 3880	. . . 4 ⊢ (𝑌 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ≠ ∅)
31	29, 30	syl 17	. . 3 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ≠ ∅)
32		0nelfil 21463	. . . . . . 7 ⊢ (𝐿 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝐿)
33	32	3ad2ant2 1076	. . . . . 6 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → ¬ ∅ ∈ 𝐿)
34	33	adantr 480	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ¬ ∅ ∈ 𝐿)
35		0ex 4718	. . . . . . 7 ⊢ ∅ ∈ V
36	11	elrnmpt 5293	. . . . . . 7 ⊢ (∅ ∈ V → (∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 ∅ = (^◡𝐹 “ 𝑥)))
37	35, 36	ax-mp 5	. . . . . 6 ⊢ (∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 ∅ = (^◡𝐹 “ 𝑥))
38		ffn 5958	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹:𝑌⟶𝑋 → 𝐹 Fn 𝑌)
39		fvelrnb 6153	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Fn 𝑌 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦))
40	38, 39	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑌⟶𝑋 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦))
41	40	3ad2ant3 1077	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦))
42	41	ad2antrr 758	. . . . . . . . . . . . . . 15 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦))
43		eleq1 2676	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑧) = 𝑦 → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑦 ∈ 𝑥))
44	43	biimparc 503	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝐹‘𝑧) = 𝑦) → (𝐹‘𝑧) ∈ 𝑥)
45	44	ad2ant2l 778	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → (𝐹‘𝑧) ∈ 𝑥)
46	45	adantll 746	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → (𝐹‘𝑧) ∈ 𝑥)
47		ffun 5961	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:𝑌⟶𝑋 → Fun 𝐹)
48	47	3ad2ant3 1077	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → Fun 𝐹)
49	48	ad3antrrr 762	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → Fun 𝐹)
50	3	eleq2d 2673	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:𝑌⟶𝑋 → (𝑧 ∈ dom 𝐹 ↔ 𝑧 ∈ 𝑌))
51	50	biimpar 501	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:𝑌⟶𝑋 ∧ 𝑧 ∈ 𝑌) → 𝑧 ∈ dom 𝐹)
52	51	3ad2antl3 1218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑧 ∈ 𝑌) → 𝑧 ∈ dom 𝐹)
53	52	adantlr 747	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑧 ∈ 𝑌) → 𝑧 ∈ dom 𝐹)
54	53	ad2ant2r 779	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → 𝑧 ∈ dom 𝐹)
55		fvimacnv 6240	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐹 ∧ 𝑧 ∈ dom 𝐹) → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑧 ∈ (^◡𝐹 “ 𝑥)))
56	49, 54, 55	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑧 ∈ (^◡𝐹 “ 𝑥)))
57	46, 56	mpbid 221	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → 𝑧 ∈ (^◡𝐹 “ 𝑥))
58		n0i 3879	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (^◡𝐹 “ 𝑥) → ¬ (^◡𝐹 “ 𝑥) = ∅)
59		eqcom 2617	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡𝐹 “ 𝑥) = ∅ ↔ ∅ = (^◡𝐹 “ 𝑥))
60	58, 59	sylnib 317	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (^◡𝐹 “ 𝑥) → ¬ ∅ = (^◡𝐹 “ 𝑥))
61	57, 60	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → ¬ ∅ = (^◡𝐹 “ 𝑥))
62	61	rexlimdvaa 3014	. . . . . . . . . . . . . . 15 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) → (∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦 → ¬ ∅ = (^◡𝐹 “ 𝑥)))
63	42, 62	sylbid 229	. . . . . . . . . . . . . 14 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) → (𝑦 ∈ ran 𝐹 → ¬ ∅ = (^◡𝐹 “ 𝑥)))
64	63	con2d 128	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) → (∅ = (^◡𝐹 “ 𝑥) → ¬ 𝑦 ∈ ran 𝐹))
65	64	expr 641	. . . . . . . . . . . 12 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → (𝑦 ∈ 𝑥 → (∅ = (^◡𝐹 “ 𝑥) → ¬ 𝑦 ∈ ran 𝐹)))
66	65	com23 84	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → (∅ = (^◡𝐹 “ 𝑥) → (𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹)))
67	66	impr 647	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → (𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹))
68	67	alrimiv 1842	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → ∀𝑦(𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹))
69		imnan 437	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ¬ (𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹))
70		elin 3758	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝑥 ∩ ran 𝐹) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹))
71	69, 70	xchbinxr 324	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
72	71	albii 1737	. . . . . . . . . 10 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ∀𝑦 ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
73		eq0 3888	. . . . . . . . . 10 ⊢ ((𝑥 ∩ ran 𝐹) = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
74		eqcom 2617	. . . . . . . . . 10 ⊢ ((𝑥 ∩ ran 𝐹) = ∅ ↔ ∅ = (𝑥 ∩ ran 𝐹))
75	72, 73, 74	3bitr2i 287	. . . . . . . . 9 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ∅ = (𝑥 ∩ ran 𝐹))
76	68, 75	sylib 207	. . . . . . . 8 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → ∅ = (𝑥 ∩ ran 𝐹))
77		simpll2 1094	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → 𝐿 ∈ (Fil‘𝑋))
78		simprl 790	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → 𝑥 ∈ 𝐿)
79		simplr 788	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → ran 𝐹 ∈ 𝐿)
80		filin 21468	. . . . . . . . 9 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝐿 ∧ ran 𝐹 ∈ 𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
81	77, 78, 79, 80	syl3anc 1318	. . . . . . . 8 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
82	76, 81	eqeltrd 2688	. . . . . . 7 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → ∅ ∈ 𝐿)
83	82	rexlimdvaa 3014	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (∃𝑥 ∈ 𝐿 ∅ = (^◡𝐹 “ 𝑥) → ∅ ∈ 𝐿))
84	37, 83	syl5bi 231	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) → ∅ ∈ 𝐿))
85	34, 84	mtod 188	. . . 4 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ¬ ∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
86		df-nel 2783	. . . 4 ⊢ (∅ ∉ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ¬ ∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
87	85, 86	sylibr 223	. . 3 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ∅ ∉ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
88		vex 3176	. . . . . . . . 9 ⊢ 𝑟 ∈ V
89	11	elrnmpt 5293	. . . . . . . . 9 ⊢ (𝑟 ∈ V → (𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑥)))
90	88, 89	ax-mp 5	. . . . . . . 8 ⊢ (𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑥))
91		imaeq2 5381	. . . . . . . . . 10 ⊢ (𝑥 = 𝑢 → (^◡𝐹 “ 𝑥) = (^◡𝐹 “ 𝑢))
92	91	eqeq2d 2620	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → (𝑟 = (^◡𝐹 “ 𝑥) ↔ 𝑟 = (^◡𝐹 “ 𝑢)))
93	92	cbvrexv 3148	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑥) ↔ ∃𝑢 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑢))
94	90, 93	bitri 263	. . . . . . 7 ⊢ (𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑢 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑢))
95		vex 3176	. . . . . . . . 9 ⊢ 𝑠 ∈ V
96	11	elrnmpt 5293	. . . . . . . . 9 ⊢ (𝑠 ∈ V → (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑥)))
97	95, 96	ax-mp 5	. . . . . . . 8 ⊢ (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑥))
98		imaeq2 5381	. . . . . . . . . 10 ⊢ (𝑥 = 𝑣 → (^◡𝐹 “ 𝑥) = (^◡𝐹 “ 𝑣))
99	98	eqeq2d 2620	. . . . . . . . 9 ⊢ (𝑥 = 𝑣 → (𝑠 = (^◡𝐹 “ 𝑥) ↔ 𝑠 = (^◡𝐹 “ 𝑣)))
100	99	cbvrexv 3148	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑥) ↔ ∃𝑣 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑣))
101	97, 100	bitri 263	. . . . . . 7 ⊢ (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑣 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑣))
102	94, 101	anbi12i 729	. . . . . 6 ⊢ ((𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ 𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ↔ (∃𝑢 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑢) ∧ ∃𝑣 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑣)))
103		reeanv 3086	. . . . . 6 ⊢ (∃𝑢 ∈ 𝐿 ∃𝑣 ∈ 𝐿 (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)) ↔ (∃𝑢 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑢) ∧ ∃𝑣 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑣)))
104	102, 103	bitr4i 266	. . . . 5 ⊢ ((𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ 𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ↔ ∃𝑢 ∈ 𝐿 ∃𝑣 ∈ 𝐿 (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))
105		filin 21468	. . . . . . . . . . . . . 14 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) → (𝑢 ∩ 𝑣) ∈ 𝐿)
106	105	3expb 1258	. . . . . . . . . . . . 13 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → (𝑢 ∩ 𝑣) ∈ 𝐿)
107	106	adantlr 747	. . . . . . . . . . . 12 ⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → (𝑢 ∩ 𝑣) ∈ 𝐿)
108		eqidd 2611	. . . . . . . . . . . 12 ⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ (𝑢 ∩ 𝑣)))
109		imaeq2 5381	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑢 ∩ 𝑣) → (^◡𝐹 “ 𝑥) = (^◡𝐹 “ (𝑢 ∩ 𝑣)))
110	109	eqeq2d 2620	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑢 ∩ 𝑣) → ((^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥) ↔ (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ (𝑢 ∩ 𝑣))))
111	110	rspcev 3282	. . . . . . . . . . . 12 ⊢ (((𝑢 ∩ 𝑣) ∈ 𝐿 ∧ (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ (𝑢 ∩ 𝑣))) → ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥))
112	107, 108, 111	syl2anc 691	. . . . . . . . . . 11 ⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥))
113	112	3adantl1 1210	. . . . . . . . . 10 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥))
114	113	ad2ant2r 779	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥))
115		simpll1 1093	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → 𝑌 ∈ 𝐴)
116		cnvimass 5404	. . . . . . . . . . . . . 14 ⊢ (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ dom 𝐹
117	116, 3	syl5sseq 3616	. . . . . . . . . . . . 13 ⊢ (𝐹:𝑌⟶𝑋 → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ 𝑌)
118	117	3ad2ant3 1077	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ 𝑌)
119	118	ad2antrr 758	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ 𝑌)
120	115, 119	ssexd 4733	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ V)
121	11	elrnmpt 5293	. . . . . . . . . 10 ⊢ ((^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ V → ((^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥)))
122	120, 121	syl 17	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → ((^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥)))
123	114, 122	mpbird 246	. . . . . . . 8 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
124		simprrl 800	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → 𝑟 = (^◡𝐹 “ 𝑢))
125		simprrr 801	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → 𝑠 = (^◡𝐹 “ 𝑣))
126	124, 125	ineq12d 3777	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (𝑟 ∩ 𝑠) = ((^◡𝐹 “ 𝑢) ∩ (^◡𝐹 “ 𝑣)))
127		funcnvcnv 5870	. . . . . . . . . . . . 13 ⊢ (Fun 𝐹 → Fun ^◡^◡𝐹)
128		imain 5888	. . . . . . . . . . . . 13 ⊢ (Fun ^◡^◡𝐹 → (^◡𝐹 “ (𝑢 ∩ 𝑣)) = ((^◡𝐹 “ 𝑢) ∩ (^◡𝐹 “ 𝑣)))
129	47, 127, 128	3syl 18	. . . . . . . . . . . 12 ⊢ (𝐹:𝑌⟶𝑋 → (^◡𝐹 “ (𝑢 ∩ 𝑣)) = ((^◡𝐹 “ 𝑢) ∩ (^◡𝐹 “ 𝑣)))
130	129	3ad2ant3 1077	. . . . . . . . . . 11 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) = ((^◡𝐹 “ 𝑢) ∩ (^◡𝐹 “ 𝑣)))
131	130	ad2antrr 758	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) = ((^◡𝐹 “ 𝑢) ∩ (^◡𝐹 “ 𝑣)))
132	126, 131	eqtr4d 2647	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (𝑟 ∩ 𝑠) = (^◡𝐹 “ (𝑢 ∩ 𝑣)))
133		eqimss2 3621	. . . . . . . . 9 ⊢ ((𝑟 ∩ 𝑠) = (^◡𝐹 “ (𝑢 ∩ 𝑣)) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠))
134	132, 133	syl 17	. . . . . . . 8 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠))
135		sseq1 3589	. . . . . . . . 9 ⊢ (𝑡 = (^◡𝐹 “ (𝑢 ∩ 𝑣)) → (𝑡 ⊆ (𝑟 ∩ 𝑠) ↔ (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠)))
136	135	rspcev 3282	. . . . . . . 8 ⊢ (((^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠)) → ∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠))
137	123, 134, 136	syl2anc 691	. . . . . . 7 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → ∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠))
138	137	exp32 629	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) → ((𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)) → ∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠))))
139	138	rexlimdvv 3019	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (∃𝑢 ∈ 𝐿 ∃𝑣 ∈ 𝐿 (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)) → ∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠)))
140	104, 139	syl5bi 231	. . . 4 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ((𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ 𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) → ∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠)))
141	140	ralrimivv 2953	. . 3 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ∀𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∀𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠))
142	31, 87, 141	3jca 1235	. 2 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ≠ ∅ ∧ ∅ ∉ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ ∀𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∀𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠)))
143		isfbas2 21449	. . 3 ⊢ (𝑌 ∈ 𝐴 → (ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌) ↔ (ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ⊆ 𝒫 𝑌 ∧ (ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ≠ ∅ ∧ ∅ ∉ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ ∀𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∀𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠)))))
144	6, 143	syl 17	. 2 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌) ↔ (ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ⊆ 𝒫 𝑌 ∧ (ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ≠ ∅ ∧ ∅ ∉ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ ∀𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∀𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠)))))
145	14, 142, 144	mpbir2and 959	1 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 ∀wal 1473 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∉ wnel 2781 ∀wral 2896 ∃wrex 2897 Vcvv 3173 ∩ cin 3539 ⊆ wss 3540 ∅c0 3874 𝒫 cpw 4108 ↦ cmpt 4643 ^◡ccnv 5037 dom cdm 5038 ran crn 5039 “ cima 5041 Fun wfun 5798 Fn wfn 5799 ⟶wf 5800 ‘cfv 5804 fBascfbas 19555 Filcfil 21459

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-fv 5812 df-fbas 19564 df-fil 21460

This theorem is referenced by: rnelfm 21567 fmfnfm 21572

W3C validator