Metamath Proof Explorer

Theorem brssc

Description: The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Assertion brssc ( 𝐻 ⊆cat 𝐽 ↔ ∃ 𝑡 ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 sscrel ⊢ Rel ⊆cat
2 1 brrelex12i ⊢ ( 𝐻 ⊆cat 𝐽 → ( 𝐻 ∈ V ∧ 𝐽 ∈ V ) )
3 vex ⊢ 𝑡 ∈ V
4 3 3 xpex ⊢ ( 𝑡 × 𝑡 ) ∈ V
5 fnex ⊢ ( ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ( 𝑡 × 𝑡 ) ∈ V ) → 𝐽 ∈ V )
6 4 5 mpan2 ⊢ ( 𝐽 Fn ( 𝑡 × 𝑡 ) → 𝐽 ∈ V )
7 elex ⊢ ( 𝐻 ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) → 𝐻 ∈ V )
8 7 rexlimivw ⊢ ( ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) → 𝐻 ∈ V )
9 6 8 anim12ci ⊢ ( ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) → ( 𝐻 ∈ V ∧ 𝐽 ∈ V ) )
10 9 exlimiv ⊢ ( ∃ 𝑡 ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) → ( 𝐻 ∈ V ∧ 𝐽 ∈ V ) )
11 simpr ⊢ ( ( ℎ = 𝐻 ∧ 𝑗 = 𝐽 ) → 𝑗 = 𝐽 )
12 11 fneq1d ⊢ ( ( ℎ = 𝐻 ∧ 𝑗 = 𝐽 ) → ( 𝑗 Fn ( 𝑡 × 𝑡 ) ↔ 𝐽 Fn ( 𝑡 × 𝑡 ) ) )
13 simpl ⊢ ( ( ℎ = 𝐻 ∧ 𝑗 = 𝐽 ) → ℎ = 𝐻 )
14 11 fveq1d ⊢ ( ( ℎ = 𝐻 ∧ 𝑗 = 𝐽 ) → ( 𝑗 ‘ 𝑥 ) = ( 𝐽 ‘ 𝑥 ) )
15 14 pweqd ⊢ ( ( ℎ = 𝐻 ∧ 𝑗 = 𝐽 ) → 𝒫 ( 𝑗 ‘ 𝑥 ) = 𝒫 ( 𝐽 ‘ 𝑥 ) )
16 15 ixpeq2dv ⊢ ( ( ℎ = 𝐻 ∧ 𝑗 = 𝐽 ) → X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝑗 ‘ 𝑥 ) = X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) )
17 13 16 eleq12d ⊢ ( ( ℎ = 𝐻 ∧ 𝑗 = 𝐽 ) → ( ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝑗 ‘ 𝑥 ) ↔ 𝐻 ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) )
18 17 rexbidv ⊢ ( ( ℎ = 𝐻 ∧ 𝑗 = 𝐽 ) → ( ∃ 𝑠 ∈ 𝒫 𝑡 ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝑗 ‘ 𝑥 ) ↔ ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) )
19 12 18 anbi12d ⊢ ( ( ℎ = 𝐻 ∧ 𝑗 = 𝐽 ) → ( ( 𝑗 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝑗 ‘ 𝑥 ) ) ↔ ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) ) )
20 19 exbidv ⊢ ( ( ℎ = 𝐻 ∧ 𝑗 = 𝐽 ) → ( ∃ 𝑡 ( 𝑗 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝑗 ‘ 𝑥 ) ) ↔ ∃ 𝑡 ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) ) )
21 df-ssc ⊢ ⊆cat = { ⟨ ℎ , 𝑗 ⟩ ∣ ∃ 𝑡 ( 𝑗 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝑗 ‘ 𝑥 ) ) }
22 20 21 brabga ⊢ ( ( 𝐻 ∈ V ∧ 𝐽 ∈ V ) → ( 𝐻 ⊆cat 𝐽 ↔ ∃ 𝑡 ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) ) )
23 2 10 22 pm5.21nii ⊢ ( 𝐻 ⊆cat 𝐽 ↔ ∃ 𝑡 ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) )