Metamath Proof Explorer


Theorem r1elss

Description: The range of the R1 function is transitive. Lemma 2.10 of Kunen p. 97. (Contributed by Mario Carneiro, 22-Mar-2013) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Hypothesis r1elss.1 AV
Assertion r1elss AR1OnAR1On

Proof

Step Hyp Ref Expression
1 r1elss.1 AV
2 r1elssi AR1OnAR1On
3 1 tz9.12 yAxOnyR1xxOnAR1x
4 dfss3 AR1OnyAyR1On
5 r1fnon R1FnOn
6 fnfun R1FnOnFunR1
7 funiunfv FunR1xOnR1x=R1On
8 5 6 7 mp2b xOnR1x=R1On
9 8 eleq2i yxOnR1xyR1On
10 eliun yxOnR1xxOnyR1x
11 9 10 bitr3i yR1OnxOnyR1x
12 11 ralbii yAyR1OnyAxOnyR1x
13 4 12 bitri AR1OnyAxOnyR1x
14 8 eleq2i AxOnR1xAR1On
15 eliun AxOnR1xxOnAR1x
16 14 15 bitr3i AR1OnxOnAR1x
17 3 13 16 3imtr4i AR1OnAR1On
18 2 17 impbii AR1OnAR1On