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 23947

Description: Lemma for rnelfm 23948. (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 1188	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝑌 ∈ 𝐴)
2		cnvimass 6091	. . . . . . 7 ⊢ (^◡𝐹 “ 𝑥) ⊆ dom 𝐹
3		simpl3 1190	. . . . . . 7 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝐹:𝑌⟶𝑋)
4	2, 3	fssdm 6747	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (^◡𝐹 “ 𝑥) ⊆ 𝑌)
5	1, 4	sselpwd 5333	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (^◡𝐹 “ 𝑥) ∈ 𝒫 𝑌)
6	5	adantr 479	. . . 4 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → (^◡𝐹 “ 𝑥) ∈ 𝒫 𝑌)
7	6	fmpttd 7129	. . 3 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)):𝐿⟶𝒫 𝑌)
8	7	frnd 6736	. 2 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ⊆ 𝒫 𝑌)
9		filtop 23850	. . . . . . . 8 ⊢ (𝐿 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐿)
10	9	3ad2ant2 1131	. . . . . . 7 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → 𝑋 ∈ 𝐿)
11	10	adantr 479	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝑋 ∈ 𝐿)
12		fimacnv 6750	. . . . . . . . 9 ⊢ (𝐹:𝑌⟶𝑋 → (^◡𝐹 “ 𝑋) = 𝑌)
13	12	eqcomd 2732	. . . . . . . 8 ⊢ (𝐹:𝑌⟶𝑋 → 𝑌 = (^◡𝐹 “ 𝑋))
14	13	3ad2ant3 1132	. . . . . . 7 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → 𝑌 = (^◡𝐹 “ 𝑋))
15	14	adantr 479	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝑌 = (^◡𝐹 “ 𝑋))
16		imaeq2 6065	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (^◡𝐹 “ 𝑥) = (^◡𝐹 “ 𝑋))
17	16	rspceeqv 3630	. . . . . 6 ⊢ ((𝑋 ∈ 𝐿 ∧ 𝑌 = (^◡𝐹 “ 𝑋)) → ∃𝑥 ∈ 𝐿 𝑌 = (^◡𝐹 “ 𝑥))
18	11, 15, 17	syl2anc 582	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ∃𝑥 ∈ 𝐿 𝑌 = (^◡𝐹 “ 𝑥))
19		eqid 2726	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) = (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))
20	19	elrnmpt 5962	. . . . . . 7 ⊢ (𝑌 ∈ 𝐴 → (𝑌 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑌 = (^◡𝐹 “ 𝑥)))
21	20	3ad2ant1 1130	. . . . . 6 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (𝑌 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑌 = (^◡𝐹 “ 𝑥)))
22	21	adantr 479	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (𝑌 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑌 = (^◡𝐹 “ 𝑥)))
23	18, 22	mpbird 256	. . . 4 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝑌 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
24	23	ne0d 4338	. . 3 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ≠ ∅)
25		0nelfil 23844	. . . . . . 7 ⊢ (𝐿 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝐿)
26	25	3ad2ant2 1131	. . . . . 6 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → ¬ ∅ ∈ 𝐿)
27	26	adantr 479	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ¬ ∅ ∈ 𝐿)
28		0ex 5312	. . . . . . 7 ⊢ ∅ ∈ V
29	19	elrnmpt 5962	. . . . . . 7 ⊢ (∅ ∈ V → (∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 ∅ = (^◡𝐹 “ 𝑥)))
30	28, 29	ax-mp 5	. . . . . 6 ⊢ (∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 ∅ = (^◡𝐹 “ 𝑥))
31		ffn 6728	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹:𝑌⟶𝑋 → 𝐹 Fn 𝑌)
32		fvelrnb 6963	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Fn 𝑌 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦))
33	31, 32	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑌⟶𝑋 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦))
34	33	3ad2ant3 1132	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦))
35	34	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦))
36		eleq1 2814	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑧) = 𝑦 → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑦 ∈ 𝑥))
37	36	biimparc 478	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝐹‘𝑧) = 𝑦) → (𝐹‘𝑧) ∈ 𝑥)
38	37	ad2ant2l 744	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → (𝐹‘𝑧) ∈ 𝑥)
39	38	adantll 712	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → (𝐹‘𝑧) ∈ 𝑥)
40		ffun 6731	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:𝑌⟶𝑋 → Fun 𝐹)
41	40	3ad2ant3 1132	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → Fun 𝐹)
42	41	ad3antrrr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → Fun 𝐹)
43		fdm 6737	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹:𝑌⟶𝑋 → dom 𝐹 = 𝑌)
44	43	eleq2d 2812	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:𝑌⟶𝑋 → (𝑧 ∈ dom 𝐹 ↔ 𝑧 ∈ 𝑌))
45	44	biimpar 476	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:𝑌⟶𝑋 ∧ 𝑧 ∈ 𝑌) → 𝑧 ∈ dom 𝐹)
46	45	3ad2antl3 1184	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑧 ∈ 𝑌) → 𝑧 ∈ dom 𝐹)
47	46	adantlr 713	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑧 ∈ 𝑌) → 𝑧 ∈ dom 𝐹)
48	47	ad2ant2r 745	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → 𝑧 ∈ dom 𝐹)
49		fvimacnv 7066	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐹 ∧ 𝑧 ∈ dom 𝐹) → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑧 ∈ (^◡𝐹 “ 𝑥)))
50	42, 48, 49	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑧 ∈ (^◡𝐹 “ 𝑥)))
51	39, 50	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → 𝑧 ∈ (^◡𝐹 “ 𝑥))
52		n0i 4336	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (^◡𝐹 “ 𝑥) → ¬ (^◡𝐹 “ 𝑥) = ∅)
53		eqcom 2733	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡𝐹 “ 𝑥) = ∅ ↔ ∅ = (^◡𝐹 “ 𝑥))
54	52, 53	sylnib 327	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (^◡𝐹 “ 𝑥) → ¬ ∅ = (^◡𝐹 “ 𝑥))
55	51, 54	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → ¬ ∅ = (^◡𝐹 “ 𝑥))
56	55	rexlimdvaa 3146	. . . . . . . . . . . . . . 15 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) → (∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦 → ¬ ∅ = (^◡𝐹 “ 𝑥)))
57	35, 56	sylbid 239	. . . . . . . . . . . . . 14 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) → (𝑦 ∈ ran 𝐹 → ¬ ∅ = (^◡𝐹 “ 𝑥)))
58	57	con2d 134	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) → (∅ = (^◡𝐹 “ 𝑥) → ¬ 𝑦 ∈ ran 𝐹))
59	58	expr 455	. . . . . . . . . . . 12 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → (𝑦 ∈ 𝑥 → (∅ = (^◡𝐹 “ 𝑥) → ¬ 𝑦 ∈ ran 𝐹)))
60	59	com23 86	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → (∅ = (^◡𝐹 “ 𝑥) → (𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹)))
61	60	impr 453	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → (𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹))
62	61	alrimiv 1923	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → ∀𝑦(𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹))
63		imnan 398	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ¬ (𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹))
64		elin 3963	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝑥 ∩ ran 𝐹) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹))
65	63, 64	xchbinxr 334	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
66	65	albii 1814	. . . . . . . . . 10 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ∀𝑦 ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
67		eq0 4346	. . . . . . . . . 10 ⊢ ((𝑥 ∩ ran 𝐹) = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
68		eqcom 2733	. . . . . . . . . 10 ⊢ ((𝑥 ∩ ran 𝐹) = ∅ ↔ ∅ = (𝑥 ∩ ran 𝐹))
69	66, 67, 68	3bitr2i 298	. . . . . . . . 9 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ∅ = (𝑥 ∩ ran 𝐹))
70	62, 69	sylib 217	. . . . . . . 8 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → ∅ = (𝑥 ∩ ran 𝐹))
71		simpll2 1210	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → 𝐿 ∈ (Fil‘𝑋))
72		simprl 769	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → 𝑥 ∈ 𝐿)
73		simplr 767	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → ran 𝐹 ∈ 𝐿)
74		filin 23849	. . . . . . . . 9 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝐿 ∧ ran 𝐹 ∈ 𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
75	71, 72, 73, 74	syl3anc 1368	. . . . . . . 8 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
76	70, 75	eqeltrd 2826	. . . . . . 7 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → ∅ ∈ 𝐿)
77	76	rexlimdvaa 3146	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (∃𝑥 ∈ 𝐿 ∅ = (^◡𝐹 “ 𝑥) → ∅ ∈ 𝐿))
78	30, 77	biimtrid 241	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) → ∅ ∈ 𝐿))
79	27, 78	mtod 197	. . . 4 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ¬ ∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
80		df-nel 3037	. . . 4 ⊢ (∅ ∉ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ¬ ∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
81	79, 80	sylibr 233	. . 3 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ∅ ∉ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
82	19	elrnmpt 5962	. . . . . . . . 9 ⊢ (𝑟 ∈ V → (𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑥)))
83	82	elv 3468	. . . . . . . 8 ⊢ (𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑥))
84		imaeq2 6065	. . . . . . . . . 10 ⊢ (𝑥 = 𝑢 → (^◡𝐹 “ 𝑥) = (^◡𝐹 “ 𝑢))
85	84	eqeq2d 2737	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → (𝑟 = (^◡𝐹 “ 𝑥) ↔ 𝑟 = (^◡𝐹 “ 𝑢)))
86	85	cbvrexvw 3226	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑥) ↔ ∃𝑢 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑢))
87	83, 86	bitri 274	. . . . . . 7 ⊢ (𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑢 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑢))
88	19	elrnmpt 5962	. . . . . . . . 9 ⊢ (𝑠 ∈ V → (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑥)))
89	88	elv 3468	. . . . . . . 8 ⊢ (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑥))
90		imaeq2 6065	. . . . . . . . . 10 ⊢ (𝑥 = 𝑣 → (^◡𝐹 “ 𝑥) = (^◡𝐹 “ 𝑣))
91	90	eqeq2d 2737	. . . . . . . . 9 ⊢ (𝑥 = 𝑣 → (𝑠 = (^◡𝐹 “ 𝑥) ↔ 𝑠 = (^◡𝐹 “ 𝑣)))
92	91	cbvrexvw 3226	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑥) ↔ ∃𝑣 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑣))
93	89, 92	bitri 274	. . . . . . 7 ⊢ (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑣 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑣))
94	87, 93	anbi12i 626	. . . . . 6 ⊢ ((𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ 𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ↔ (∃𝑢 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑢) ∧ ∃𝑣 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑣)))
95		reeanv 3217	. . . . . 6 ⊢ (∃𝑢 ∈ 𝐿 ∃𝑣 ∈ 𝐿 (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)) ↔ (∃𝑢 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑢) ∧ ∃𝑣 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑣)))
96	94, 95	bitr4i 277	. . . . 5 ⊢ ((𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ 𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ↔ ∃𝑢 ∈ 𝐿 ∃𝑣 ∈ 𝐿 (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))
97		filin 23849	. . . . . . . . . . . . . 14 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) → (𝑢 ∩ 𝑣) ∈ 𝐿)
98	97	3expb 1117	. . . . . . . . . . . . 13 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → (𝑢 ∩ 𝑣) ∈ 𝐿)
99	98	adantlr 713	. . . . . . . . . . . 12 ⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → (𝑢 ∩ 𝑣) ∈ 𝐿)
100		eqidd 2727	. . . . . . . . . . . 12 ⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ (𝑢 ∩ 𝑣)))
101		imaeq2 6065	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑢 ∩ 𝑣) → (^◡𝐹 “ 𝑥) = (^◡𝐹 “ (𝑢 ∩ 𝑣)))
102	101	rspceeqv 3630	. . . . . . . . . . . 12 ⊢ (((𝑢 ∩ 𝑣) ∈ 𝐿 ∧ (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ (𝑢 ∩ 𝑣))) → ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥))
103	99, 100, 102	syl2anc 582	. . . . . . . . . . 11 ⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥))
104	103	3adantl1 1163	. . . . . . . . . 10 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥))
105	104	ad2ant2r 745	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥))
106		simpll1 1209	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → 𝑌 ∈ 𝐴)
107		cnvimass 6091	. . . . . . . . . . . . . 14 ⊢ (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ dom 𝐹
108	107, 43	sseqtrid 4032	. . . . . . . . . . . . 13 ⊢ (𝐹:𝑌⟶𝑋 → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ 𝑌)
109	108	3ad2ant3 1132	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ 𝑌)
110	109	ad2antrr 724	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ 𝑌)
111	106, 110	ssexd 5329	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ V)
112	19	elrnmpt 5962	. . . . . . . . . 10 ⊢ ((^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ V → ((^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥)))
113	111, 112	syl 17	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → ((^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥)))
114	105, 113	mpbird 256	. . . . . . . 8 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
115		simprrl 779	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → 𝑟 = (^◡𝐹 “ 𝑢))
116		simprrr 780	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → 𝑠 = (^◡𝐹 “ 𝑣))
117	115, 116	ineq12d 4214	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (𝑟 ∩ 𝑠) = ((^◡𝐹 “ 𝑢) ∩ (^◡𝐹 “ 𝑣)))
118		funcnvcnv 6626	. . . . . . . . . . . . 13 ⊢ (Fun 𝐹 → Fun ^◡^◡𝐹)
119		imain 6644	. . . . . . . . . . . . 13 ⊢ (Fun ^◡^◡𝐹 → (^◡𝐹 “ (𝑢 ∩ 𝑣)) = ((^◡𝐹 “ 𝑢) ∩ (^◡𝐹 “ 𝑣)))
120	40, 118, 119	3syl 18	. . . . . . . . . . . 12 ⊢ (𝐹:𝑌⟶𝑋 → (^◡𝐹 “ (𝑢 ∩ 𝑣)) = ((^◡𝐹 “ 𝑢) ∩ (^◡𝐹 “ 𝑣)))
121	120	3ad2ant3 1132	. . . . . . . . . . 11 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) = ((^◡𝐹 “ 𝑢) ∩ (^◡𝐹 “ 𝑣)))
122	121	ad2antrr 724	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) = ((^◡𝐹 “ 𝑢) ∩ (^◡𝐹 “ 𝑣)))
123	117, 122	eqtr4d 2769	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (𝑟 ∩ 𝑠) = (^◡𝐹 “ (𝑢 ∩ 𝑣)))
124		eqimss2 4039	. . . . . . . . 9 ⊢ ((𝑟 ∩ 𝑠) = (^◡𝐹 “ (𝑢 ∩ 𝑣)) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠))
125	123, 124	syl 17	. . . . . . . 8 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠))
126		sseq1 4005	. . . . . . . . 9 ⊢ (𝑡 = (^◡𝐹 “ (𝑢 ∩ 𝑣)) → (𝑡 ⊆ (𝑟 ∩ 𝑠) ↔ (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠)))
127	126	rspcev 3608	. . . . . . . 8 ⊢ (((^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠)) → ∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠))
128	114, 125, 127	syl2anc 582	. . . . . . 7 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → ∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠))
129	128	exp32 419	. . . . . 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 3189	. . 3 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ∀𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∀𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠))
133	24, 81, 132	3jca 1125	. 2 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ≠ ∅ ∧ ∅ ∉ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ ∀𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∀𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠)))
134		isfbas2 23830	. . 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 394 ∧ w3a 1084 ∀wal 1532 = wceq 1534 ∈ wcel 2099 ≠ wne 2930 ∉ wnel 3036 ∀wral 3051 ∃wrex 3060 Vcvv 3462 ∩ cin 3946 ⊆ wss 3947 ∅c0 4325 𝒫 cpw 4607 ↦ cmpt 5236 ^◡ccnv 5681 dom cdm 5682 ran crn 5683 “ cima 5685 Fun wfun 6548 Fn wfn 6549 ⟶wf 6550 ‘cfv 6554 fBascfbas 21331 Filcfil 23840

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-sep 5304 ax-nul 5311 ax-pow 5369 ax-pr 5433

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3464 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4326 df-if 4534 df-pw 4609 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-br 5154 df-opab 5216 df-mpt 5237 df-id 5580 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-iota 6506 df-fun 6556 df-fn 6557 df-f 6558 df-fv 6562 df-fbas 21340 df-fil 23841

This theorem is referenced by: rnelfm 23948 fmfnfm 23953

W3C validator