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 23209

Description: Lemma for rnelfm 23210. (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 1191	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝑌 ∈ 𝐴)
2		cnvimass 6024	. . . . . . 7 ⊢ (^◡𝐹 “ 𝑥) ⊆ dom 𝐹
3		simpl3 1193	. . . . . . 7 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝐹:𝑌⟶𝑋)
4	2, 3	fssdm 6676	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (^◡𝐹 “ 𝑥) ⊆ 𝑌)
5	1, 4	sselpwd 5275	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (^◡𝐹 “ 𝑥) ∈ 𝒫 𝑌)
6	5	adantr 482	. . . 4 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → (^◡𝐹 “ 𝑥) ∈ 𝒫 𝑌)
7	6	fmpttd 7050	. . 3 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)):𝐿⟶𝒫 𝑌)
8	7	frnd 6664	. 2 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ⊆ 𝒫 𝑌)
9		filtop 23112	. . . . . . . 8 ⊢ (𝐿 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐿)
10	9	3ad2ant2 1134	. . . . . . 7 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → 𝑋 ∈ 𝐿)
11	10	adantr 482	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝑋 ∈ 𝐿)
12		fimacnv 6678	. . . . . . . . 9 ⊢ (𝐹:𝑌⟶𝑋 → (^◡𝐹 “ 𝑋) = 𝑌)
13	12	eqcomd 2743	. . . . . . . 8 ⊢ (𝐹:𝑌⟶𝑋 → 𝑌 = (^◡𝐹 “ 𝑋))
14	13	3ad2ant3 1135	. . . . . . 7 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → 𝑌 = (^◡𝐹 “ 𝑋))
15	14	adantr 482	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝑌 = (^◡𝐹 “ 𝑋))
16		imaeq2 6000	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (^◡𝐹 “ 𝑥) = (^◡𝐹 “ 𝑋))
17	16	rspceeqv 3588	. . . . . 6 ⊢ ((𝑋 ∈ 𝐿 ∧ 𝑌 = (^◡𝐹 “ 𝑋)) → ∃𝑥 ∈ 𝐿 𝑌 = (^◡𝐹 “ 𝑥))
18	11, 15, 17	syl2anc 585	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ∃𝑥 ∈ 𝐿 𝑌 = (^◡𝐹 “ 𝑥))
19		eqid 2737	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) = (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))
20	19	elrnmpt 5902	. . . . . . 7 ⊢ (𝑌 ∈ 𝐴 → (𝑌 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑌 = (^◡𝐹 “ 𝑥)))
21	20	3ad2ant1 1133	. . . . . 6 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (𝑌 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑌 = (^◡𝐹 “ 𝑥)))
22	21	adantr 482	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (𝑌 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑌 = (^◡𝐹 “ 𝑥)))
23	18, 22	mpbird 257	. . . 4 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝑌 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
24	23	ne0d 4287	. . 3 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ≠ ∅)
25		0nelfil 23106	. . . . . . 7 ⊢ (𝐿 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝐿)
26	25	3ad2ant2 1134	. . . . . 6 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → ¬ ∅ ∈ 𝐿)
27	26	adantr 482	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ¬ ∅ ∈ 𝐿)
28		0ex 5256	. . . . . . 7 ⊢ ∅ ∈ V
29	19	elrnmpt 5902	. . . . . . 7 ⊢ (∅ ∈ V → (∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 ∅ = (^◡𝐹 “ 𝑥)))
30	28, 29	ax-mp 5	. . . . . 6 ⊢ (∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 ∅ = (^◡𝐹 “ 𝑥))
31		ffn 6656	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹:𝑌⟶𝑋 → 𝐹 Fn 𝑌)
32		fvelrnb 6891	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Fn 𝑌 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦))
33	31, 32	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑌⟶𝑋 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦))
34	33	3ad2ant3 1135	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦))
35	34	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦))
36		eleq1 2825	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑧) = 𝑦 → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑦 ∈ 𝑥))
37	36	biimparc 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝐹‘𝑧) = 𝑦) → (𝐹‘𝑧) ∈ 𝑥)
38	37	ad2ant2l 744	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → (𝐹‘𝑧) ∈ 𝑥)
39	38	adantll 712	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → (𝐹‘𝑧) ∈ 𝑥)
40		ffun 6659	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:𝑌⟶𝑋 → Fun 𝐹)
41	40	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → Fun 𝐹)
42	41	ad3antrrr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → Fun 𝐹)
43		fdm 6665	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹:𝑌⟶𝑋 → dom 𝐹 = 𝑌)
44	43	eleq2d 2823	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:𝑌⟶𝑋 → (𝑧 ∈ dom 𝐹 ↔ 𝑧 ∈ 𝑌))
45	44	biimpar 479	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:𝑌⟶𝑋 ∧ 𝑧 ∈ 𝑌) → 𝑧 ∈ dom 𝐹)
46	45	3ad2antl3 1187	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑧 ∈ 𝑌) → 𝑧 ∈ dom 𝐹)
47	46	adantlr 713	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑧 ∈ 𝑌) → 𝑧 ∈ dom 𝐹)
48	47	ad2ant2r 745	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → 𝑧 ∈ dom 𝐹)
49		fvimacnv 6991	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐹 ∧ 𝑧 ∈ dom 𝐹) → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑧 ∈ (^◡𝐹 “ 𝑥)))
50	42, 48, 49	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑧 ∈ (^◡𝐹 “ 𝑥)))
51	39, 50	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → 𝑧 ∈ (^◡𝐹 “ 𝑥))
52		n0i 4285	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (^◡𝐹 “ 𝑥) → ¬ (^◡𝐹 “ 𝑥) = ∅)
53		eqcom 2744	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡𝐹 “ 𝑥) = ∅ ↔ ∅ = (^◡𝐹 “ 𝑥))
54	52, 53	sylnib 328	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (^◡𝐹 “ 𝑥) → ¬ ∅ = (^◡𝐹 “ 𝑥))
55	51, 54	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → ¬ ∅ = (^◡𝐹 “ 𝑥))
56	55	rexlimdvaa 3150	. . . . . . . . . . . . . . 15 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) → (∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦 → ¬ ∅ = (^◡𝐹 “ 𝑥)))
57	35, 56	sylbid 239	. . . . . . . . . . . . . 14 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) → (𝑦 ∈ ran 𝐹 → ¬ ∅ = (^◡𝐹 “ 𝑥)))
58	57	con2d 134	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) → (∅ = (^◡𝐹 “ 𝑥) → ¬ 𝑦 ∈ ran 𝐹))
59	58	expr 458	. . . . . . . . . . . 12 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → (𝑦 ∈ 𝑥 → (∅ = (^◡𝐹 “ 𝑥) → ¬ 𝑦 ∈ ran 𝐹)))
60	59	com23 86	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → (∅ = (^◡𝐹 “ 𝑥) → (𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹)))
61	60	impr 456	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → (𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹))
62	61	alrimiv 1930	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → ∀𝑦(𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹))
63		imnan 401	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ¬ (𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹))
64		elin 3918	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝑥 ∩ ran 𝐹) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹))
65	63, 64	xchbinxr 335	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
66	65	albii 1821	. . . . . . . . . 10 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ∀𝑦 ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
67		eq0 4295	. . . . . . . . . 10 ⊢ ((𝑥 ∩ ran 𝐹) = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
68		eqcom 2744	. . . . . . . . . 10 ⊢ ((𝑥 ∩ ran 𝐹) = ∅ ↔ ∅ = (𝑥 ∩ ran 𝐹))
69	66, 67, 68	3bitr2i 299	. . . . . . . . 9 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ∅ = (𝑥 ∩ ran 𝐹))
70	62, 69	sylib 217	. . . . . . . 8 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → ∅ = (𝑥 ∩ ran 𝐹))
71		simpll2 1213	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → 𝐿 ∈ (Fil‘𝑋))
72		simprl 769	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → 𝑥 ∈ 𝐿)
73		simplr 767	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → ran 𝐹 ∈ 𝐿)
74		filin 23111	. . . . . . . . 9 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝐿 ∧ ran 𝐹 ∈ 𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
75	71, 72, 73, 74	syl3anc 1371	. . . . . . . 8 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
76	70, 75	eqeltrd 2838	. . . . . . 7 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → ∅ ∈ 𝐿)
77	76	rexlimdvaa 3150	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (∃𝑥 ∈ 𝐿 ∅ = (^◡𝐹 “ 𝑥) → ∅ ∈ 𝐿))
78	30, 77	biimtrid 241	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) → ∅ ∈ 𝐿))
79	27, 78	mtod 197	. . . 4 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ¬ ∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
80		df-nel 3048	. . . 4 ⊢ (∅ ∉ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ¬ ∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
81	79, 80	sylibr 233	. . 3 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ∅ ∉ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
82	19	elrnmpt 5902	. . . . . . . . 9 ⊢ (𝑟 ∈ V → (𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑥)))
83	82	elv 3448	. . . . . . . 8 ⊢ (𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑥))
84		imaeq2 6000	. . . . . . . . . 10 ⊢ (𝑥 = 𝑢 → (^◡𝐹 “ 𝑥) = (^◡𝐹 “ 𝑢))
85	84	eqeq2d 2748	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → (𝑟 = (^◡𝐹 “ 𝑥) ↔ 𝑟 = (^◡𝐹 “ 𝑢)))
86	85	cbvrexvw 3223	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑥) ↔ ∃𝑢 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑢))
87	83, 86	bitri 275	. . . . . . 7 ⊢ (𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑢 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑢))
88	19	elrnmpt 5902	. . . . . . . . 9 ⊢ (𝑠 ∈ V → (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑥)))
89	88	elv 3448	. . . . . . . 8 ⊢ (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑥))
90		imaeq2 6000	. . . . . . . . . 10 ⊢ (𝑥 = 𝑣 → (^◡𝐹 “ 𝑥) = (^◡𝐹 “ 𝑣))
91	90	eqeq2d 2748	. . . . . . . . 9 ⊢ (𝑥 = 𝑣 → (𝑠 = (^◡𝐹 “ 𝑥) ↔ 𝑠 = (^◡𝐹 “ 𝑣)))
92	91	cbvrexvw 3223	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑥) ↔ ∃𝑣 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑣))
93	89, 92	bitri 275	. . . . . . 7 ⊢ (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑣 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑣))
94	87, 93	anbi12i 628	. . . . . 6 ⊢ ((𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ 𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ↔ (∃𝑢 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑢) ∧ ∃𝑣 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑣)))
95		reeanv 3214	. . . . . 6 ⊢ (∃𝑢 ∈ 𝐿 ∃𝑣 ∈ 𝐿 (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)) ↔ (∃𝑢 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑢) ∧ ∃𝑣 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑣)))
96	94, 95	bitr4i 278	. . . . 5 ⊢ ((𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ 𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ↔ ∃𝑢 ∈ 𝐿 ∃𝑣 ∈ 𝐿 (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))
97		filin 23111	. . . . . . . . . . . . . 14 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) → (𝑢 ∩ 𝑣) ∈ 𝐿)
98	97	3expb 1120	. . . . . . . . . . . . 13 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → (𝑢 ∩ 𝑣) ∈ 𝐿)
99	98	adantlr 713	. . . . . . . . . . . 12 ⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → (𝑢 ∩ 𝑣) ∈ 𝐿)
100		eqidd 2738	. . . . . . . . . . . 12 ⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ (𝑢 ∩ 𝑣)))
101		imaeq2 6000	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑢 ∩ 𝑣) → (^◡𝐹 “ 𝑥) = (^◡𝐹 “ (𝑢 ∩ 𝑣)))
102	101	rspceeqv 3588	. . . . . . . . . . . 12 ⊢ (((𝑢 ∩ 𝑣) ∈ 𝐿 ∧ (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ (𝑢 ∩ 𝑣))) → ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥))
103	99, 100, 102	syl2anc 585	. . . . . . . . . . 11 ⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥))
104	103	3adantl1 1166	. . . . . . . . . 10 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥))
105	104	ad2ant2r 745	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥))
106		simpll1 1212	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → 𝑌 ∈ 𝐴)
107		cnvimass 6024	. . . . . . . . . . . . . 14 ⊢ (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ dom 𝐹
108	107, 43	sseqtrid 3988	. . . . . . . . . . . . 13 ⊢ (𝐹:𝑌⟶𝑋 → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ 𝑌)
109	108	3ad2ant3 1135	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ 𝑌)
110	109	ad2antrr 724	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ 𝑌)
111	106, 110	ssexd 5273	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ V)
112	19	elrnmpt 5902	. . . . . . . . . 10 ⊢ ((^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ V → ((^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥)))
113	111, 112	syl 17	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → ((^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥)))
114	105, 113	mpbird 257	. . . . . . . 8 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
115		simprrl 779	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → 𝑟 = (^◡𝐹 “ 𝑢))
116		simprrr 780	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → 𝑠 = (^◡𝐹 “ 𝑣))
117	115, 116	ineq12d 4165	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (𝑟 ∩ 𝑠) = ((^◡𝐹 “ 𝑢) ∩ (^◡𝐹 “ 𝑣)))
118		funcnvcnv 6556	. . . . . . . . . . . . 13 ⊢ (Fun 𝐹 → Fun ^◡^◡𝐹)
119		imain 6574	. . . . . . . . . . . . 13 ⊢ (Fun ^◡^◡𝐹 → (^◡𝐹 “ (𝑢 ∩ 𝑣)) = ((^◡𝐹 “ 𝑢) ∩ (^◡𝐹 “ 𝑣)))
120	40, 118, 119	3syl 18	. . . . . . . . . . . 12 ⊢ (𝐹:𝑌⟶𝑋 → (^◡𝐹 “ (𝑢 ∩ 𝑣)) = ((^◡𝐹 “ 𝑢) ∩ (^◡𝐹 “ 𝑣)))
121	120	3ad2ant3 1135	. . . . . . . . . . 11 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) = ((^◡𝐹 “ 𝑢) ∩ (^◡𝐹 “ 𝑣)))
122	121	ad2antrr 724	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) = ((^◡𝐹 “ 𝑢) ∩ (^◡𝐹 “ 𝑣)))
123	117, 122	eqtr4d 2780	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (𝑟 ∩ 𝑠) = (^◡𝐹 “ (𝑢 ∩ 𝑣)))
124		eqimss2 3993	. . . . . . . . 9 ⊢ ((𝑟 ∩ 𝑠) = (^◡𝐹 “ (𝑢 ∩ 𝑣)) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠))
125	123, 124	syl 17	. . . . . . . 8 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠))
126		sseq1 3961	. . . . . . . . 9 ⊢ (𝑡 = (^◡𝐹 “ (𝑢 ∩ 𝑣)) → (𝑡 ⊆ (𝑟 ∩ 𝑠) ↔ (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠)))
127	126	rspcev 3574	. . . . . . . 8 ⊢ (((^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠)) → ∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠))
128	114, 125, 127	syl2anc 585	. . . . . . 7 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → ∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠))
129	128	exp32 422	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) → ((𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)) → ∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠))))
130	129	rexlimdvv 3201	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (∃𝑢 ∈ 𝐿 ∃𝑣 ∈ 𝐿 (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)) → ∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠)))
131	96, 130	biimtrid 241	. . . 4 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ((𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ 𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) → ∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠)))
132	131	ralrimivv 3192	. . 3 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ∀𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∀𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠))
133	24, 81, 132	3jca 1128	. 2 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ≠ ∅ ∧ ∅ ∉ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ ∀𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∀𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠)))
134		isfbas2 23092	. . 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 711	1 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1087 ∀wal 1539 = wceq 1541 ∈ wcel 2106 ≠ wne 2941 ∉ wnel 3047 ∀wral 3062 ∃wrex 3071 Vcvv 3442 ∩ cin 3901 ⊆ wss 3902 ∅c0 4274 𝒫 cpw 4552 ↦ cmpt 5180 ^◡ccnv 5624 dom cdm 5625 ran crn 5626 “ cima 5628 Fun wfun 6478 Fn wfn 6479 ⟶wf 6480 ‘cfv 6484 fBascfbas 20691 Filcfil 23102

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 ax-sep 5248 ax-nul 5255 ax-pow 5313 ax-pr 5377

This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rab 3405 df-v 3444 df-sbc 3732 df-csb 3848 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4275 df-if 4479 df-pw 4554 df-sn 4579 df-pr 4581 df-op 4585 df-uni 4858 df-br 5098 df-opab 5160 df-mpt 5181 df-id 5523 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-iota 6436 df-fun 6486 df-fn 6487 df-f 6488 df-fv 6492 df-fbas 20700 df-fil 23103

This theorem is referenced by: rnelfm 23210 fmfnfm 23215

W3C validator