Metamath Proof Explorer

Theorem gneispace

Description: The predicate that F is a (generic) Seifert and Threlfall neighborhood space. (Contributed by RP, 14-Apr-2021)

Ref Expression
Hypothesis gneispace.a ⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : dom 𝑓 ⟶ ( 𝒫 ( 𝒫 dom 𝑓 ∖ { ∅ } ) ∖ { ∅ } ) ∧ ∀ 𝑝 ∈ dom 𝑓 ∀ 𝑛 ∈ ( 𝑓 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝑓 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝑓 ‘ 𝑝 ) ) ) ) }
Assertion gneispace ( 𝐹 ∈ 𝑉 → ( 𝐹 ∈ 𝐴 ↔ ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gneispace.a ⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : dom 𝑓 ⟶ ( 𝒫 ( 𝒫 dom 𝑓 ∖ { ∅ } ) ∖ { ∅ } ) ∧ ∀ 𝑝 ∈ dom 𝑓 ∀ 𝑛 ∈ ( 𝑓 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝑓 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝑓 ‘ 𝑝 ) ) ) ) }
2 1 gneispace3 ⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∈ 𝐴 ↔ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) ∧ ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) )
3 simpll ⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) ∧ ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) → Fun 𝐹 )
4 simplr ⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) ∧ ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) → ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) )
5 difss ⊢ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ⊆ 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } )
6 difss ⊢ ( 𝒫 dom 𝐹 ∖ { ∅ } ) ⊆ 𝒫 dom 𝐹
7 6 sspwi ⊢ 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ⊆ 𝒫 𝒫 dom 𝐹
8 5 7 sstri ⊢ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ⊆ 𝒫 𝒫 dom 𝐹
9 4 8 sstrdi ⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) ∧ ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) → ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 )
10 simpr ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) → ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) )
11 simpl ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) → Fun 𝐹 )
12 fvelrn ⊢ ( ( Fun 𝐹 ∧ 𝑝 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑝 ) ∈ ran 𝐹 )
13 11 12 sylan ⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) ∧ 𝑝 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑝 ) ∈ ran 𝐹 )
14 ssel2 ⊢ ( ( ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ∧ ( 𝐹 ‘ 𝑝 ) ∈ ran 𝐹 ) → ( 𝐹 ‘ 𝑝 ) ∈ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) )
15 eldifsni ⊢ ( ( 𝐹 ‘ 𝑝 ) ∈ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) → ( 𝐹 ‘ 𝑝 ) ≠ ∅ )
16 14 15 syl ⊢ ( ( ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ∧ ( 𝐹 ‘ 𝑝 ) ∈ ran 𝐹 ) → ( 𝐹 ‘ 𝑝 ) ≠ ∅ )
17 10 13 16 syl2an2r ⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) ∧ 𝑝 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑝 ) ≠ ∅ )
18 17 ralrimiva ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) → ∀ 𝑝 ∈ dom 𝐹 ( 𝐹 ‘ 𝑝 ) ≠ ∅ )
19 r19.26 ⊢ ( ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ↔ ( ∀ 𝑝 ∈ dom 𝐹 ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) )
20 19 biimpri ⊢ ( ( ∀ 𝑝 ∈ dom 𝐹 ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) → ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) )
21 18 20 sylan ⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) ∧ ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) → ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) )
22 3 9 21 3jca ⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) ∧ ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) → ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) )
23 simp1 ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → Fun 𝐹 )
24 nfv ⊢ Ⅎ 𝑝 Fun 𝐹
25 nfv ⊢ Ⅎ 𝑝 ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹
26 nfra1 ⊢ Ⅎ 𝑝 ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) )
27 24 25 26 nf3an ⊢ Ⅎ 𝑝 ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) )
28 simpr ⊢ ( ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) → ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) )
29 simpl ⊢ ( ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) → 𝑝 ∈ 𝑛 )
30 29 19.8ad ⊢ ( ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) → ∃ 𝑝 𝑝 ∈ 𝑛 )
31 30 ralimi ⊢ ( ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) → ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ∃ 𝑝 𝑝 ∈ 𝑛 )
32 28 31 syl ⊢ ( ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) → ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ∃ 𝑝 𝑝 ∈ 𝑛 )
33 32 ralimi ⊢ ( ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) → ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ∃ 𝑝 𝑝 ∈ 𝑛 )
34 33 3ad2ant3 ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ∃ 𝑝 𝑝 ∈ 𝑛 )
35 rsp ⊢ ( ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ∃ 𝑝 𝑝 ∈ 𝑛 → ( 𝑝 ∈ dom 𝐹 → ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ∃ 𝑝 𝑝 ∈ 𝑛 ) )
36 34 35 syl ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → ( 𝑝 ∈ dom 𝐹 → ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ∃ 𝑝 𝑝 ∈ 𝑛 ) )
37 df-ex ⊢ ( ∃ 𝑝 𝑝 ∈ 𝑛 ↔ ¬ ∀ 𝑝 ¬ 𝑝 ∈ 𝑛 )
38 37 ralbii ⊢ ( ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ∃ 𝑝 𝑝 ∈ 𝑛 ↔ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ¬ ∀ 𝑝 ¬ 𝑝 ∈ 𝑛 )
39 ralnex ⊢ ( ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ¬ ∀ 𝑝 ¬ 𝑝 ∈ 𝑛 ↔ ¬ ∃ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ∀ 𝑝 ¬ 𝑝 ∈ 𝑛 )
40 38 39 bitri ⊢ ( ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ∃ 𝑝 𝑝 ∈ 𝑛 ↔ ¬ ∃ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ∀ 𝑝 ¬ 𝑝 ∈ 𝑛 )
41 0el ⊢ ( ∅ ∈ ( 𝐹 ‘ 𝑝 ) ↔ ∃ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ∀ 𝑝 ¬ 𝑝 ∈ 𝑛 )
42 40 41 xchbinxr ⊢ ( ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ∃ 𝑝 𝑝 ∈ 𝑛 ↔ ¬ ∅ ∈ ( 𝐹 ‘ 𝑝 ) )
43 42 biimpi ⊢ ( ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ∃ 𝑝 𝑝 ∈ 𝑛 → ¬ ∅ ∈ ( 𝐹 ‘ 𝑝 ) )
44 elinel1 ⊢ ( ∅ ∈ ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) → ∅ ∈ ( 𝐹 ‘ 𝑝 ) )
45 43 44 nsyl ⊢ ( ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ∃ 𝑝 𝑝 ∈ 𝑛 → ¬ ∅ ∈ ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) )
46 disjsn ⊢ ( ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) ∩ { ∅ } ) = ∅ ↔ ¬ ∅ ∈ ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) )
47 45 46 sylibr ⊢ ( ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ∃ 𝑝 𝑝 ∈ 𝑛 → ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) ∩ { ∅ } ) = ∅ )
48 disjdif2 ⊢ ( ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) ∩ { ∅ } ) = ∅ → ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) ∖ { ∅ } ) = ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) )
49 47 48 syl ⊢ ( ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ∃ 𝑝 𝑝 ∈ 𝑛 → ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) ∖ { ∅ } ) = ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) )
50 36 49 syl6 ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → ( 𝑝 ∈ dom 𝐹 → ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) ∖ { ∅ } ) = ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) ) )
51 simp2 ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 )
52 12 ex ⊢ ( Fun 𝐹 → ( 𝑝 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑝 ) ∈ ran 𝐹 ) )
53 23 52 syl ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → ( 𝑝 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑝 ) ∈ ran 𝐹 ) )
54 ssel2 ⊢ ( ( ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ( 𝐹 ‘ 𝑝 ) ∈ ran 𝐹 ) → ( 𝐹 ‘ 𝑝 ) ∈ 𝒫 𝒫 dom 𝐹 )
55 fvex ⊢ ( 𝐹 ‘ 𝑝 ) ∈ V
56 55 elpw ⊢ ( ( 𝐹 ‘ 𝑝 ) ∈ 𝒫 𝒫 dom 𝐹 ↔ ( 𝐹 ‘ 𝑝 ) ⊆ 𝒫 dom 𝐹 )
57 df-ss ⊢ ( ( 𝐹 ‘ 𝑝 ) ⊆ 𝒫 dom 𝐹 ↔ ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) = ( 𝐹 ‘ 𝑝 ) )
58 56 57 sylbb ⊢ ( ( 𝐹 ‘ 𝑝 ) ∈ 𝒫 𝒫 dom 𝐹 → ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) = ( 𝐹 ‘ 𝑝 ) )
59 54 58 syl ⊢ ( ( ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ( 𝐹 ‘ 𝑝 ) ∈ ran 𝐹 ) → ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) = ( 𝐹 ‘ 𝑝 ) )
60 51 53 59 syl6an ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → ( 𝑝 ∈ dom 𝐹 → ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) = ( 𝐹 ‘ 𝑝 ) ) )
61 50 60 jcad ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → ( 𝑝 ∈ dom 𝐹 → ( ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) ∖ { ∅ } ) = ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) ∧ ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) = ( 𝐹 ‘ 𝑝 ) ) ) )
62 eqtr ⊢ ( ( ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) ∖ { ∅ } ) = ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) ∧ ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) = ( 𝐹 ‘ 𝑝 ) ) → ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) ∖ { ∅ } ) = ( 𝐹 ‘ 𝑝 ) )
63 df-ss ⊢ ( ( 𝐹 ‘ 𝑝 ) ⊆ ( 𝒫 dom 𝐹 ∖ { ∅ } ) ↔ ( ( 𝐹 ‘ 𝑝 ) ∩ ( 𝒫 dom 𝐹 ∖ { ∅ } ) ) = ( 𝐹 ‘ 𝑝 ) )
64 indif2 ⊢ ( ( 𝐹 ‘ 𝑝 ) ∩ ( 𝒫 dom 𝐹 ∖ { ∅ } ) ) = ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) ∖ { ∅ } )
65 64 eqeq1i ⊢ ( ( ( 𝐹 ‘ 𝑝 ) ∩ ( 𝒫 dom 𝐹 ∖ { ∅ } ) ) = ( 𝐹 ‘ 𝑝 ) ↔ ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) ∖ { ∅ } ) = ( 𝐹 ‘ 𝑝 ) )
66 63 65 bitri ⊢ ( ( 𝐹 ‘ 𝑝 ) ⊆ ( 𝒫 dom 𝐹 ∖ { ∅ } ) ↔ ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) ∖ { ∅ } ) = ( 𝐹 ‘ 𝑝 ) )
67 62 66 sylibr ⊢ ( ( ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) ∖ { ∅ } ) = ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) ∧ ( ( 𝐹 ‘ 𝑝 ) ∩ 𝒫 dom 𝐹 ) = ( 𝐹 ‘ 𝑝 ) ) → ( 𝐹 ‘ 𝑝 ) ⊆ ( 𝒫 dom 𝐹 ∖ { ∅ } ) )
68 61 67 syl6 ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → ( 𝑝 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑝 ) ⊆ ( 𝒫 dom 𝐹 ∖ { ∅ } ) ) )
69 27 68 ralrimi ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → ∀ 𝑝 ∈ dom 𝐹 ( 𝐹 ‘ 𝑝 ) ⊆ ( 𝒫 dom 𝐹 ∖ { ∅ } ) )
70 23 funfnd ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → 𝐹 Fn dom 𝐹 )
71 sseq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑝 ) → ( 𝑥 ⊆ ( 𝒫 dom 𝐹 ∖ { ∅ } ) ↔ ( 𝐹 ‘ 𝑝 ) ⊆ ( 𝒫 dom 𝐹 ∖ { ∅ } ) ) )
72 71 ralrn ⊢ ( 𝐹 Fn dom 𝐹 → ( ∀ 𝑥 ∈ ran 𝐹 𝑥 ⊆ ( 𝒫 dom 𝐹 ∖ { ∅ } ) ↔ ∀ 𝑝 ∈ dom 𝐹 ( 𝐹 ‘ 𝑝 ) ⊆ ( 𝒫 dom 𝐹 ∖ { ∅ } ) ) )
73 70 72 syl ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → ( ∀ 𝑥 ∈ ran 𝐹 𝑥 ⊆ ( 𝒫 dom 𝐹 ∖ { ∅ } ) ↔ ∀ 𝑝 ∈ dom 𝐹 ( 𝐹 ‘ 𝑝 ) ⊆ ( 𝒫 dom 𝐹 ∖ { ∅ } ) ) )
74 69 73 mpbird ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → ∀ 𝑥 ∈ ran 𝐹 𝑥 ⊆ ( 𝒫 dom 𝐹 ∖ { ∅ } ) )
75 pwssb ⊢ ( ran 𝐹 ⊆ 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ↔ ∀ 𝑥 ∈ ran 𝐹 𝑥 ⊆ ( 𝒫 dom 𝐹 ∖ { ∅ } ) )
76 74 75 sylibr ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → ran 𝐹 ⊆ 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) )
77 simpl ⊢ ( ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) → ( 𝐹 ‘ 𝑝 ) ≠ ∅ )
78 77 ralimi ⊢ ( ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) → ∀ 𝑝 ∈ dom 𝐹 ( 𝐹 ‘ 𝑝 ) ≠ ∅ )
79 78 3ad2ant3 ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → ∀ 𝑝 ∈ dom 𝐹 ( 𝐹 ‘ 𝑝 ) ≠ ∅ )
80 23 79 jca ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → ( Fun 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( 𝐹 ‘ 𝑝 ) ≠ ∅ ) )
81 elrnrexdm ⊢ ( Fun 𝐹 → ( ∅ ∈ ran 𝐹 → ∃ 𝑝 ∈ dom 𝐹 ∅ = ( 𝐹 ‘ 𝑝 ) ) )
82 nesym ⊢ ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ↔ ¬ ∅ = ( 𝐹 ‘ 𝑝 ) )
83 82 ralbii ⊢ ( ∀ 𝑝 ∈ dom 𝐹 ( 𝐹 ‘ 𝑝 ) ≠ ∅ ↔ ∀ 𝑝 ∈ dom 𝐹 ¬ ∅ = ( 𝐹 ‘ 𝑝 ) )
84 ralnex ⊢ ( ∀ 𝑝 ∈ dom 𝐹 ¬ ∅ = ( 𝐹 ‘ 𝑝 ) ↔ ¬ ∃ 𝑝 ∈ dom 𝐹 ∅ = ( 𝐹 ‘ 𝑝 ) )
85 83 84 sylbb ⊢ ( ∀ 𝑝 ∈ dom 𝐹 ( 𝐹 ‘ 𝑝 ) ≠ ∅ → ¬ ∃ 𝑝 ∈ dom 𝐹 ∅ = ( 𝐹 ‘ 𝑝 ) )
86 81 85 nsyli ⊢ ( Fun 𝐹 → ( ∀ 𝑝 ∈ dom 𝐹 ( 𝐹 ‘ 𝑝 ) ≠ ∅ → ¬ ∅ ∈ ran 𝐹 ) )
87 86 imp ⊢ ( ( Fun 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( 𝐹 ‘ 𝑝 ) ≠ ∅ ) → ¬ ∅ ∈ ran 𝐹 )
88 disjsn ⊢ ( ( ran 𝐹 ∩ { ∅ } ) = ∅ ↔ ¬ ∅ ∈ ran 𝐹 )
89 87 88 sylibr ⊢ ( ( Fun 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( 𝐹 ‘ 𝑝 ) ≠ ∅ ) → ( ran 𝐹 ∩ { ∅ } ) = ∅ )
90 80 89 syl ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → ( ran 𝐹 ∩ { ∅ } ) = ∅ )
91 reldisj ⊢ ( ran 𝐹 ⊆ 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) → ( ( ran 𝐹 ∩ { ∅ } ) = ∅ ↔ ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) )
92 91 biimpd ⊢ ( ran 𝐹 ⊆ 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) → ( ( ran 𝐹 ∩ { ∅ } ) = ∅ → ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) )
93 76 90 92 sylc ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) )
94 23 93 jca ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) )
95 19 biimpi ⊢ ( ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) → ( ∀ 𝑝 ∈ dom 𝐹 ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) )
96 95 3ad2ant3 ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → ( ∀ 𝑝 ∈ dom 𝐹 ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) )
97 simpr ⊢ ( ( ∀ 𝑝 ∈ dom 𝐹 ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) → ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) )
98 96 97 syl ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) )
99 94 98 jca ⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) ∧ ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) )
100 22 99 impbii ⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) ∧ ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ↔ ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) )
101 2 100 bitrdi ⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∈ 𝐴 ↔ ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) ) )