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 24078

Description: Lemma for rnelfm 24079. (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 1208	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝑌 ∈ 𝐴)
2		cnvimass 6085	. . . . . . 7 ⊢ (^◡𝐹 “ 𝑥) ⊆ dom 𝐹
3		simpl3 1210	. . . . . . 7 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝐹:𝑌⟶𝑋)
4	2, 3	fssdm 6726	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (^◡𝐹 “ 𝑥) ⊆ 𝑌)
5	1, 4	sselpwd 5299	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (^◡𝐹 “ 𝑥) ∈ 𝒫 𝑌)
6	5	adantr 485	. . . 4 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → (^◡𝐹 “ 𝑥) ∈ 𝒫 𝑌)
7	6	fmpttd 7111	. . 3 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)):𝐿⟶𝒫 𝑌)
8	7	frnd 6715	. 2 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ⊆ 𝒫 𝑌)
9		filtop 23981	. . . . . . . 8 ⊢ (𝐿 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐿)
10	9	3ad2ant2 1150	. . . . . . 7 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → 𝑋 ∈ 𝐿)
11	10	adantr 485	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝑋 ∈ 𝐿)
12		fimacnv 6729	. . . . . . . . 9 ⊢ (𝐹:𝑌⟶𝑋 → (^◡𝐹 “ 𝑋) = 𝑌)
13	12	eqcomd 2775	. . . . . . . 8 ⊢ (𝐹:𝑌⟶𝑋 → 𝑌 = (^◡𝐹 “ 𝑋))
14	13	3ad2ant3 1151	. . . . . . 7 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → 𝑌 = (^◡𝐹 “ 𝑋))
15	14	adantr 485	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝑌 = (^◡𝐹 “ 𝑋))
16		imaeq2 6059	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (^◡𝐹 “ 𝑥) = (^◡𝐹 “ 𝑋))
17	16	rspceeqv 3613	. . . . . 6 ⊢ ((𝑋 ∈ 𝐿 ∧ 𝑌 = (^◡𝐹 “ 𝑋)) → ∃𝑥 ∈ 𝐿 𝑌 = (^◡𝐹 “ 𝑥))
18	11, 15, 17	syl2anc 595	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ∃𝑥 ∈ 𝐿 𝑌 = (^◡𝐹 “ 𝑥))
19		eqid 2769	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) = (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))
20	19	elrnmpt 5949	. . . . . . 7 ⊢ (𝑌 ∈ 𝐴 → (𝑌 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑌 = (^◡𝐹 “ 𝑥)))
21	20	3ad2ant1 1149	. . . . . 6 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (𝑌 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑌 = (^◡𝐹 “ 𝑥)))
22	21	adantr 485	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (𝑌 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑌 = (^◡𝐹 “ 𝑥)))
23	18, 22	mpbird 260	. . . 4 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → 𝑌 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
24	23	ne0d 4303	. . 3 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ≠ ∅)
25		0nelfil 23975	. . . . . . 7 ⊢ (𝐿 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝐿)
26	25	3ad2ant2 1150	. . . . . 6 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → ¬ ∅ ∈ 𝐿)
27	26	adantr 485	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ¬ ∅ ∈ 𝐿)
28		0ex 5272	. . . . . . 7 ⊢ ∅ ∈ V
29	19	elrnmpt 5949	. . . . . . 7 ⊢ (∅ ∈ V → (∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 ∅ = (^◡𝐹 “ 𝑥)))
30	28, 29	ax-mp 5	. . . . . 6 ⊢ (∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 ∅ = (^◡𝐹 “ 𝑥))
31		ffn 6706	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹:𝑌⟶𝑋 → 𝐹 Fn 𝑌)
32		fvelrnb 6942	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Fn 𝑌 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦))
33	31, 32	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑌⟶𝑋 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦))
34	33	3ad2ant3 1151	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦))
35	34	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦))
36		eleq1 2857	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑧) = 𝑦 → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑦 ∈ 𝑥))
37	36	biimparc 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝐹‘𝑧) = 𝑦) → (𝐹‘𝑧) ∈ 𝑥)
38	37	ad2ant2l 758	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → (𝐹‘𝑧) ∈ 𝑥)
39	38	adantll 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → (𝐹‘𝑧) ∈ 𝑥)
40		ffun 6709	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:𝑌⟶𝑋 → Fun 𝐹)
41	40	3ad2ant3 1151	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → Fun 𝐹)
42	41	ad3antrrr 742	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → Fun 𝐹)
43		fdm 6716	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹:𝑌⟶𝑋 → dom 𝐹 = 𝑌)
44	43	eleq2d 2855	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:𝑌⟶𝑋 → (𝑧 ∈ dom 𝐹 ↔ 𝑧 ∈ 𝑌))
45	44	biimpar 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:𝑌⟶𝑋 ∧ 𝑧 ∈ 𝑌) → 𝑧 ∈ dom 𝐹)
46	45	3ad2antl3 1204	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑧 ∈ 𝑌) → 𝑧 ∈ dom 𝐹)
47	46	adantlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑧 ∈ 𝑌) → 𝑧 ∈ dom 𝐹)
48	47	ad2ant2r 759	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → 𝑧 ∈ dom 𝐹)
49		fvimacnv 7049	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐹 ∧ 𝑧 ∈ dom 𝐹) → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑧 ∈ (^◡𝐹 “ 𝑥)))
50	42, 48, 49	syl2anc 595	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑧 ∈ (^◡𝐹 “ 𝑥)))
51	39, 50	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → 𝑧 ∈ (^◡𝐹 “ 𝑥))
52		n0i 4301	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (^◡𝐹 “ 𝑥) → ¬ (^◡𝐹 “ 𝑥) = ∅)
53		eqcom 2776	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡𝐹 “ 𝑥) = ∅ ↔ ∅ = (^◡𝐹 “ 𝑥))
54	52, 53	sylnib 331	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (^◡𝐹 “ 𝑥) → ¬ ∅ = (^◡𝐹 “ 𝑥))
55	51, 54	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑧 ∈ 𝑌 ∧ (𝐹‘𝑧) = 𝑦)) → ¬ ∅ = (^◡𝐹 “ 𝑥))
56	55	rexlimdvaa 3173	. . . . . . . . . . . . . . 15 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) → (∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦 → ¬ ∅ = (^◡𝐹 “ 𝑥)))
57	35, 56	sylbid 243	. . . . . . . . . . . . . 14 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) → (𝑦 ∈ ran 𝐹 → ¬ ∅ = (^◡𝐹 “ 𝑥)))
58	57	con2d 135	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ 𝑦 ∈ 𝑥)) → (∅ = (^◡𝐹 “ 𝑥) → ¬ 𝑦 ∈ ran 𝐹))
59	58	expr 461	. . . . . . . . . . . 12 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → (𝑦 ∈ 𝑥 → (∅ = (^◡𝐹 “ 𝑥) → ¬ 𝑦 ∈ ran 𝐹)))
60	59	com23 87	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → (∅ = (^◡𝐹 “ 𝑥) → (𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹)))
61	60	impr 459	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → (𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹))
62	61	alrimiv 1954	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → ∀𝑦(𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹))
63		imnan 404	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ¬ (𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹))
64		elin 3929	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝑥 ∩ ran 𝐹) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹))
65	63, 64	xchbinxr 338	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
66	65	albii 1846	. . . . . . . . . 10 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ∀𝑦 ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
67		eq0 4312	. . . . . . . . . 10 ⊢ ((𝑥 ∩ ran 𝐹) = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ (𝑥 ∩ ran 𝐹))
68		eqcom 2776	. . . . . . . . . 10 ⊢ ((𝑥 ∩ ran 𝐹) = ∅ ↔ ∅ = (𝑥 ∩ ran 𝐹))
69	66, 67, 68	3bitr2i 302	. . . . . . . . 9 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ ran 𝐹) ↔ ∅ = (𝑥 ∩ ran 𝐹))
70	62, 69	sylib 221	. . . . . . . 8 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → ∅ = (𝑥 ∩ ran 𝐹))
71		simpll2 1230	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → 𝐿 ∈ (Fil‘𝑋))
72		simprl 782	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → 𝑥 ∈ 𝐿)
73		simplr 780	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → ran 𝐹 ∈ 𝐿)
74		filin 23980	. . . . . . . . 9 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝐿 ∧ ran 𝐹 ∈ 𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
75	71, 72, 73, 74	syl3anc 1396	. . . . . . . 8 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → (𝑥 ∩ ran 𝐹) ∈ 𝐿)
76	70, 75	eqeltrd 2869	. . . . . . 7 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ (𝑥 ∈ 𝐿 ∧ ∅ = (^◡𝐹 “ 𝑥))) → ∅ ∈ 𝐿)
77	76	rexlimdvaa 3173	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (∃𝑥 ∈ 𝐿 ∅ = (^◡𝐹 “ 𝑥) → ∅ ∈ 𝐿))
78	30, 77	biimtrid 245	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) → ∅ ∈ 𝐿))
79	27, 78	mtod 201	. . . 4 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ¬ ∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
80		df-nel 3071	. . . 4 ⊢ (∅ ∉ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ¬ ∅ ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
81	79, 80	sylibr 237	. . 3 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ∅ ∉ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
82	19	elrnmpt 5949	. . . . . . . . 9 ⊢ (𝑟 ∈ V → (𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑥)))
83	82	elv 3468	. . . . . . . 8 ⊢ (𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑥))
84		imaeq2 6059	. . . . . . . . . 10 ⊢ (𝑥 = 𝑢 → (^◡𝐹 “ 𝑥) = (^◡𝐹 “ 𝑢))
85	84	eqeq2d 2780	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → (𝑟 = (^◡𝐹 “ 𝑥) ↔ 𝑟 = (^◡𝐹 “ 𝑢)))
86	85	cbvrexvw 3250	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑥) ↔ ∃𝑢 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑢))
87	83, 86	bitri 278	. . . . . . 7 ⊢ (𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑢 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑢))
88	19	elrnmpt 5949	. . . . . . . . 9 ⊢ (𝑠 ∈ V → (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑥)))
89	88	elv 3468	. . . . . . . 8 ⊢ (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑥))
90		imaeq2 6059	. . . . . . . . . 10 ⊢ (𝑥 = 𝑣 → (^◡𝐹 “ 𝑥) = (^◡𝐹 “ 𝑣))
91	90	eqeq2d 2780	. . . . . . . . 9 ⊢ (𝑥 = 𝑣 → (𝑠 = (^◡𝐹 “ 𝑥) ↔ 𝑠 = (^◡𝐹 “ 𝑣)))
92	91	cbvrexvw 3250	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑥) ↔ ∃𝑣 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑣))
93	89, 92	bitri 278	. . . . . . 7 ⊢ (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑣 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑣))
94	87, 93	anbi12i 639	. . . . . 6 ⊢ ((𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ 𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ↔ (∃𝑢 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑢) ∧ ∃𝑣 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑣)))
95		reeanv 3243	. . . . . 6 ⊢ (∃𝑢 ∈ 𝐿 ∃𝑣 ∈ 𝐿 (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)) ↔ (∃𝑢 ∈ 𝐿 𝑟 = (^◡𝐹 “ 𝑢) ∧ ∃𝑣 ∈ 𝐿 𝑠 = (^◡𝐹 “ 𝑣)))
96	94, 95	bitr4i 281	. . . . 5 ⊢ ((𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ 𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ↔ ∃𝑢 ∈ 𝐿 ∃𝑣 ∈ 𝐿 (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))
97		filin 23980	. . . . . . . . . . . . . 14 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) → (𝑢 ∩ 𝑣) ∈ 𝐿)
98	97	3expb 1136	. . . . . . . . . . . . 13 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → (𝑢 ∩ 𝑣) ∈ 𝐿)
99	98	adantlr 727	. . . . . . . . . . . 12 ⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → (𝑢 ∩ 𝑣) ∈ 𝐿)
100		eqidd 2770	. . . . . . . . . . . 12 ⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ (𝑢 ∩ 𝑣)))
101		imaeq2 6059	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑢 ∩ 𝑣) → (^◡𝐹 “ 𝑥) = (^◡𝐹 “ (𝑢 ∩ 𝑣)))
102	101	rspceeqv 3613	. . . . . . . . . . . 12 ⊢ (((𝑢 ∩ 𝑣) ∈ 𝐿 ∧ (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ (𝑢 ∩ 𝑣))) → ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥))
103	99, 100, 102	syl2anc 595	. . . . . . . . . . 11 ⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥))
104	103	3adantl1 1183	. . . . . . . . . 10 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿)) → ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥))
105	104	ad2ant2r 759	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥))
106		simpll1 1229	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → 𝑌 ∈ 𝐴)
107		cnvimass 6085	. . . . . . . . . . . . . 14 ⊢ (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ dom 𝐹
108	107, 43	sseqtrid 3987	. . . . . . . . . . . . 13 ⊢ (𝐹:𝑌⟶𝑋 → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ 𝑌)
109	108	3ad2ant3 1151	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ 𝑌)
110	109	ad2antrr 738	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ 𝑌)
111	106, 110	ssexd 5295	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ V)
112	19	elrnmpt 5949	. . . . . . . . . 10 ⊢ ((^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ V → ((^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥)))
113	111, 112	syl 18	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → ((^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (^◡𝐹 “ (𝑢 ∩ 𝑣)) = (^◡𝐹 “ 𝑥)))
114	105, 113	mpbird 260	. . . . . . . 8 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
115		simprrl 792	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → 𝑟 = (^◡𝐹 “ 𝑢))
116		simprrr 793	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → 𝑠 = (^◡𝐹 “ 𝑣))
117	115, 116	ineq12d 4182	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (𝑟 ∩ 𝑠) = ((^◡𝐹 “ 𝑢) ∩ (^◡𝐹 “ 𝑣)))
118		funcnvcnv 6604	. . . . . . . . . . . . 13 ⊢ (Fun 𝐹 → Fun ^◡^◡𝐹)
119		imain 6622	. . . . . . . . . . . . 13 ⊢ (Fun ^◡^◡𝐹 → (^◡𝐹 “ (𝑢 ∩ 𝑣)) = ((^◡𝐹 “ 𝑢) ∩ (^◡𝐹 “ 𝑣)))
120	40, 118, 119	3syl 19	. . . . . . . . . . . 12 ⊢ (𝐹:𝑌⟶𝑋 → (^◡𝐹 “ (𝑢 ∩ 𝑣)) = ((^◡𝐹 “ 𝑢) ∩ (^◡𝐹 “ 𝑣)))
121	120	3ad2ant3 1151	. . . . . . . . . . 11 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) = ((^◡𝐹 “ 𝑢) ∩ (^◡𝐹 “ 𝑣)))
122	121	ad2antrr 738	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) = ((^◡𝐹 “ 𝑢) ∩ (^◡𝐹 “ 𝑣)))
123	117, 122	eqtr4d 2807	. . . . . . . . 9 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (𝑟 ∩ 𝑠) = (^◡𝐹 “ (𝑢 ∩ 𝑣)))
124		eqimss2 4004	. . . . . . . . 9 ⊢ ((𝑟 ∩ 𝑠) = (^◡𝐹 “ (𝑢 ∩ 𝑣)) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠))
125	123, 124	syl 18	. . . . . . . 8 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠))
126		sseq1 3970	. . . . . . . . 9 ⊢ (𝑡 = (^◡𝐹 “ (𝑢 ∩ 𝑣)) → (𝑡 ⊆ (𝑟 ∩ 𝑠) ↔ (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠)))
127	126	rspcev 3590	. . . . . . . 8 ⊢ (((^◡𝐹 “ (𝑢 ∩ 𝑣)) ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ (^◡𝐹 “ (𝑢 ∩ 𝑣)) ⊆ (𝑟 ∩ 𝑠)) → ∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠))
128	114, 125, 127	syl2anc 595	. . . . . . 7 ⊢ ((((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) ∧ ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) ∧ (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)))) → ∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠))
129	128	exp32 425	. . . . . 6 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ((𝑢 ∈ 𝐿 ∧ 𝑣 ∈ 𝐿) → ((𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)) → ∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠))))
130	129	rexlimdvv 3227	. . . . 5 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (∃𝑢 ∈ 𝐿 ∃𝑣 ∈ 𝐿 (𝑟 = (^◡𝐹 “ 𝑢) ∧ 𝑠 = (^◡𝐹 “ 𝑣)) → ∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠)))
131	96, 130	biimtrid 245	. . . 4 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ((𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ 𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) → ∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠)))
132	131	ralrimivv 3212	. . 3 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ∀𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∀𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠))
133	24, 81, 132	3jca 1144	. 2 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ≠ ∅ ∧ ∅ ∉ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ ∀𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∀𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠)))
134		isfbas2 23961	. . 3 ⊢ (𝑌 ∈ 𝐴 → (ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌) ↔ (ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ⊆ 𝒫 𝑌 ∧ (ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ≠ ∅ ∧ ∅ ∉ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ ∀𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∀𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠)))))
135	1, 134	syl 18	. 2 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → (ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌) ↔ (ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ⊆ 𝒫 𝑌 ∧ (ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ≠ ∅ ∧ ∅ ∉ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∧ ∀𝑟 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∀𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))∃𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))𝑡 ⊆ (𝑟 ∩ 𝑠)))))
136	8, 133, 135	mpbir2and 725	1 ⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 ∀wal 1565 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 ∉ wnel 3070 ∀wral 3085 ∃wrex 3095 Vcvv 3463 ∩ cin 3912 ⊆ wss 3913 ∅c0 4294 𝒫 cpw 4567 ↦ cmpt 5196 ^◡ccnv 5661 dom cdm 5662 ran crn 5663 “ cima 5665 Fun wfun 6531 Fn wfn 6532 ⟶wf 6533 ‘cfv 6537 fBascfbas 21479 Filcfil 23971

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-br 5114 df-opab 5178 df-mpt 5197 df-id 5557 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-fv 6545 df-fbas 21488 df-fil 23972

This theorem is referenced by: rnelfm 24079 fmfnfm 24084

W3C validator