Metamath Proof Explorer

Theorem ufldom

Description: The ultrafilter lemma property is a cardinal invariant, so since it transfers to subsets it also transfers over set dominance. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion ufldom ( ( 𝑋 ∈ UFL ∧ 𝑌 ≼ 𝑋 ) → 𝑌 ∈ UFL )

Proof

Step Hyp Ref Expression
1 domeng ⊢ ( 𝑋 ∈ UFL → ( 𝑌 ≼ 𝑋 ↔ ∃ 𝑥 ( 𝑌 ≈ 𝑥 ∧ 𝑥 ⊆ 𝑋 ) ) )
2 bren ⊢ ( 𝑌 ≈ 𝑥 ↔ ∃ 𝑓 𝑓 : 𝑌 –1-1-onto→ 𝑥 )
3 2 biimpi ⊢ ( 𝑌 ≈ 𝑥 → ∃ 𝑓 𝑓 : 𝑌 –1-1-onto→ 𝑥 )
4 ssufl ⊢ ( ( 𝑋 ∈ UFL ∧ 𝑥 ⊆ 𝑋 ) → 𝑥 ∈ UFL )
5 simplr ⊢ ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) → 𝑥 ∈ UFL )
6 filfbas ⊢ ( 𝑔 ∈ ( Fil ‘ 𝑌 ) → 𝑔 ∈ ( fBas ‘ 𝑌 ) )
7 6 adantl ⊢ ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) → 𝑔 ∈ ( fBas ‘ 𝑌 ) )
8 f1of ⊢ ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 → 𝑓 : 𝑌 ⟶ 𝑥 )
9 8 ad2antrr ⊢ ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) → 𝑓 : 𝑌 ⟶ 𝑥 )
10 fmfil ⊢ ( ( 𝑥 ∈ UFL ∧ 𝑔 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑓 : 𝑌 ⟶ 𝑥 ) → ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ∈ ( Fil ‘ 𝑥 ) )
11 5 7 9 10 syl3anc ⊢ ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) → ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ∈ ( Fil ‘ 𝑥 ) )
12 ufli ⊢ ( ( 𝑥 ∈ UFL ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ∈ ( Fil ‘ 𝑥 ) ) → ∃ 𝑦 ∈ ( UFil ‘ 𝑥 ) ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 )
13 5 11 12 syl2anc ⊢ ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) → ∃ 𝑦 ∈ ( UFil ‘ 𝑥 ) ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 )
14 f1odm ⊢ ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 → dom 𝑓 = 𝑌 )
15 14 adantr ⊢ ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) → dom 𝑓 = 𝑌 )
16 vex ⊢ 𝑓 ∈ V
17 16 dmex ⊢ dom 𝑓 ∈ V
18 15 17 eqeltrrdi ⊢ ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) → 𝑌 ∈ V )
19 18 ad2antrr ⊢ ( ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → 𝑌 ∈ V )
20 simprl ⊢ ( ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → 𝑦 ∈ ( UFil ‘ 𝑥 ) )
21 f1ocnv ⊢ ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 → ◡ 𝑓 : 𝑥 –1-1-onto→ 𝑌 )
22 21 ad3antrrr ⊢ ( ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → ◡ 𝑓 : 𝑥 –1-1-onto→ 𝑌 )
23 f1of ⊢ ( ◡ 𝑓 : 𝑥 –1-1-onto→ 𝑌 → ◡ 𝑓 : 𝑥 ⟶ 𝑌 )
24 22 23 syl ⊢ ( ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → ◡ 𝑓 : 𝑥 ⟶ 𝑌 )
25 fmufil ⊢ ( ( 𝑌 ∈ V ∧ 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ◡ 𝑓 : 𝑥 ⟶ 𝑌 ) → ( ( 𝑌 FilMap ◡ 𝑓 ) ‘ 𝑦 ) ∈ ( UFil ‘ 𝑌 ) )
26 19 20 24 25 syl3anc ⊢ ( ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → ( ( 𝑌 FilMap ◡ 𝑓 ) ‘ 𝑦 ) ∈ ( UFil ‘ 𝑌 ) )
27 f1ococnv1 ⊢ ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 → ( ◡ 𝑓 ∘ 𝑓 ) = ( I ↾ 𝑌 ) )
28 27 ad3antrrr ⊢ ( ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → ( ◡ 𝑓 ∘ 𝑓 ) = ( I ↾ 𝑌 ) )
29 28 oveq2d ⊢ ( ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → ( 𝑌 FilMap ( ◡ 𝑓 ∘ 𝑓 ) ) = ( 𝑌 FilMap ( I ↾ 𝑌 ) ) )
30 29 fveq1d ⊢ ( ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → ( ( 𝑌 FilMap ( ◡ 𝑓 ∘ 𝑓 ) ) ‘ 𝑔 ) = ( ( 𝑌 FilMap ( I ↾ 𝑌 ) ) ‘ 𝑔 ) )
31 5 adantr ⊢ ( ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → 𝑥 ∈ UFL )
32 7 adantr ⊢ ( ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → 𝑔 ∈ ( fBas ‘ 𝑌 ) )
33 8 ad3antrrr ⊢ ( ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → 𝑓 : 𝑌 ⟶ 𝑥 )
34 fmco ⊢ ( ( ( 𝑌 ∈ V ∧ 𝑥 ∈ UFL ∧ 𝑔 ∈ ( fBas ‘ 𝑌 ) ) ∧ ( ◡ 𝑓 : 𝑥 ⟶ 𝑌 ∧ 𝑓 : 𝑌 ⟶ 𝑥 ) ) → ( ( 𝑌 FilMap ( ◡ 𝑓 ∘ 𝑓 ) ) ‘ 𝑔 ) = ( ( 𝑌 FilMap ◡ 𝑓 ) ‘ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ) )
35 19 31 32 24 33 34 syl32anc ⊢ ( ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → ( ( 𝑌 FilMap ( ◡ 𝑓 ∘ 𝑓 ) ) ‘ 𝑔 ) = ( ( 𝑌 FilMap ◡ 𝑓 ) ‘ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ) )
36 simplr ⊢ ( ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → 𝑔 ∈ ( Fil ‘ 𝑌 ) )
37 fmid ⊢ ( 𝑔 ∈ ( Fil ‘ 𝑌 ) → ( ( 𝑌 FilMap ( I ↾ 𝑌 ) ) ‘ 𝑔 ) = 𝑔 )
38 36 37 syl ⊢ ( ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → ( ( 𝑌 FilMap ( I ↾ 𝑌 ) ) ‘ 𝑔 ) = 𝑔 )
39 30 35 38 3eqtr3d ⊢ ( ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → ( ( 𝑌 FilMap ◡ 𝑓 ) ‘ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ) = 𝑔 )
40 11 adantr ⊢ ( ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ∈ ( Fil ‘ 𝑥 ) )
41 filfbas ⊢ ( ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ∈ ( Fil ‘ 𝑥 ) → ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ∈ ( fBas ‘ 𝑥 ) )
42 40 41 syl ⊢ ( ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ∈ ( fBas ‘ 𝑥 ) )
43 ufilfil ⊢ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) → 𝑦 ∈ ( Fil ‘ 𝑥 ) )
44 filfbas ⊢ ( 𝑦 ∈ ( Fil ‘ 𝑥 ) → 𝑦 ∈ ( fBas ‘ 𝑥 ) )
45 20 43 44 3syl ⊢ ( ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → 𝑦 ∈ ( fBas ‘ 𝑥 ) )
46 simprr ⊢ ( ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 )
47 fmss ⊢ ( ( ( 𝑌 ∈ V ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ∈ ( fBas ‘ 𝑥 ) ∧ 𝑦 ∈ ( fBas ‘ 𝑥 ) ) ∧ ( ◡ 𝑓 : 𝑥 ⟶ 𝑌 ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → ( ( 𝑌 FilMap ◡ 𝑓 ) ‘ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ) ⊆ ( ( 𝑌 FilMap ◡ 𝑓 ) ‘ 𝑦 ) )
48 19 42 45 24 46 47 syl32anc ⊢ ( ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → ( ( 𝑌 FilMap ◡ 𝑓 ) ‘ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ) ⊆ ( ( 𝑌 FilMap ◡ 𝑓 ) ‘ 𝑦 ) )
49 39 48 eqsstrrd ⊢ ( ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → 𝑔 ⊆ ( ( 𝑌 FilMap ◡ 𝑓 ) ‘ 𝑦 ) )
50 sseq2 ⊢ ( 𝑢 = ( ( 𝑌 FilMap ◡ 𝑓 ) ‘ 𝑦 ) → ( 𝑔 ⊆ 𝑢 ↔ 𝑔 ⊆ ( ( 𝑌 FilMap ◡ 𝑓 ) ‘ 𝑦 ) ) )
51 50 rspcev ⊢ ( ( ( ( 𝑌 FilMap ◡ 𝑓 ) ‘ 𝑦 ) ∈ ( UFil ‘ 𝑌 ) ∧ 𝑔 ⊆ ( ( 𝑌 FilMap ◡ 𝑓 ) ‘ 𝑦 ) ) → ∃ 𝑢 ∈ ( UFil ‘ 𝑌 ) 𝑔 ⊆ 𝑢 )
52 26 49 51 syl2anc ⊢ ( ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ ( UFil ‘ 𝑥 ) ∧ ( ( 𝑥 FilMap 𝑓 ) ‘ 𝑔 ) ⊆ 𝑦 ) ) → ∃ 𝑢 ∈ ( UFil ‘ 𝑌 ) 𝑔 ⊆ 𝑢 )
53 13 52 rexlimddv ⊢ ( ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) ∧ 𝑔 ∈ ( Fil ‘ 𝑌 ) ) → ∃ 𝑢 ∈ ( UFil ‘ 𝑌 ) 𝑔 ⊆ 𝑢 )
54 53 ralrimiva ⊢ ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) → ∀ 𝑔 ∈ ( Fil ‘ 𝑌 ) ∃ 𝑢 ∈ ( UFil ‘ 𝑌 ) 𝑔 ⊆ 𝑢 )
55 isufl ⊢ ( 𝑌 ∈ V → ( 𝑌 ∈ UFL ↔ ∀ 𝑔 ∈ ( Fil ‘ 𝑌 ) ∃ 𝑢 ∈ ( UFil ‘ 𝑌 ) 𝑔 ⊆ 𝑢 ) )
56 18 55 syl ⊢ ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) → ( 𝑌 ∈ UFL ↔ ∀ 𝑔 ∈ ( Fil ‘ 𝑌 ) ∃ 𝑢 ∈ ( UFil ‘ 𝑌 ) 𝑔 ⊆ 𝑢 ) )
57 54 56 mpbird ⊢ ( ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) → 𝑌 ∈ UFL )
58 57 ex ⊢ ( 𝑓 : 𝑌 –1-1-onto→ 𝑥 → ( 𝑥 ∈ UFL → 𝑌 ∈ UFL ) )
59 58 exlimiv ⊢ ( ∃ 𝑓 𝑓 : 𝑌 –1-1-onto→ 𝑥 → ( 𝑥 ∈ UFL → 𝑌 ∈ UFL ) )
60 59 imp ⊢ ( ( ∃ 𝑓 𝑓 : 𝑌 –1-1-onto→ 𝑥 ∧ 𝑥 ∈ UFL ) → 𝑌 ∈ UFL )
61 3 4 60 syl2an ⊢ ( ( 𝑌 ≈ 𝑥 ∧ ( 𝑋 ∈ UFL ∧ 𝑥 ⊆ 𝑋 ) ) → 𝑌 ∈ UFL )
62 61 an12s ⊢ ( ( 𝑋 ∈ UFL ∧ ( 𝑌 ≈ 𝑥 ∧ 𝑥 ⊆ 𝑋 ) ) → 𝑌 ∈ UFL )
63 62 ex ⊢ ( 𝑋 ∈ UFL → ( ( 𝑌 ≈ 𝑥 ∧ 𝑥 ⊆ 𝑋 ) → 𝑌 ∈ UFL ) )
64 63 exlimdv ⊢ ( 𝑋 ∈ UFL → ( ∃ 𝑥 ( 𝑌 ≈ 𝑥 ∧ 𝑥 ⊆ 𝑋 ) → 𝑌 ∈ UFL ) )
65 1 64 sylbid ⊢ ( 𝑋 ∈ UFL → ( 𝑌 ≼ 𝑋 → 𝑌 ∈ UFL ) )
66 65 imp ⊢ ( ( 𝑋 ∈ UFL ∧ 𝑌 ≼ 𝑋 ) → 𝑌 ∈ UFL )